Skip to content

Commit

Permalink
fix: do not use the defaults for nat_cast and int_cast fields on …
Browse files Browse the repository at this point in the history
…pi instances (#1185)

This creates a diamond, since we populate these fields manually on other instances. This error was introduced in the port and was not present in mathlib3.
  • Loading branch information
eric-wieser committed Dec 23, 2022
1 parent 71723d8 commit 1cd86c9
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions Mathlib/Algebra/Ring/Pi.lean
Expand Up @@ -50,7 +50,7 @@ instance nonUnitalSemiring [∀ i, NonUnitalSemiring <| f i] : NonUnitalSemiring
#align pi.non_unital_semiring Pi.nonUnitalSemiring

instance nonAssocSemiring [∀ i, NonAssocSemiring <| f i] : NonAssocSemiring (∀ i : I, f i) :=
{ Pi.nonUnitalNonAssocSemiring, Pi.mulZeroOneClass with }
{ Pi.nonUnitalNonAssocSemiring, Pi.mulZeroOneClass, Pi.addMonoidWithOne with }
#align pi.non_assoc_semiring Pi.nonAssocSemiring

instance semiring [∀ i, Semiring <| f i] : Semiring (∀ i : I, f i) :=
Expand All @@ -76,7 +76,7 @@ instance nonUnitalRing [∀ i, NonUnitalRing <| f i] : NonUnitalRing (∀ i : I,
#align pi.non_unital_ring Pi.nonUnitalRing

instance nonAssocRing [∀ i, NonAssocRing <| f i] : NonAssocRing (∀ i : I, f i) :=
{ Pi.nonUnitalNonAssocRing, Pi.nonAssocSemiring with }
{ Pi.nonUnitalNonAssocRing, Pi.nonAssocSemiring, Pi.addGroupWithOne with }
#align pi.non_assoc_ring Pi.nonAssocRing

instance ring [∀ i, Ring <| f i] : Ring (∀ i : I, f i) :=
Expand Down

0 comments on commit 1cd86c9

Please sign in to comment.