Skip to content

Commit

Permalink
fix(Equiv/TransferInstance): move to_additive attribute (#11277)
Browse files Browse the repository at this point in the history
Removes `to_additive` from a `MulZeroClass` instance and instead puts it on the corresponding `MulOneClass` instance (more explanation here: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/to_additive.20on.20MulZeroClass).
  • Loading branch information
chrisflav authored and dagurtomas committed Mar 22, 2024
1 parent 9456d78 commit 366a5f2
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/Logic/Equiv/TransferInstance.lean
Original file line number Diff line number Diff line change
Expand Up @@ -265,7 +265,6 @@ protected def mulZeroClass [MulZeroClass β] : MulZeroClass α := by
apply e.injective.mulZeroClass _ <;> intros <;> exact e.apply_symm_apply _
#align equiv.mul_zero_class Equiv.mulZeroClass

@[to_additive]
noncomputable instance [Small.{v} α] [MulZeroClass α] : MulZeroClass (Shrink.{v} α) :=
(equivShrink α).symm.mulZeroClass

Expand All @@ -278,6 +277,7 @@ protected def mulOneClass [MulOneClass β] : MulOneClass α := by
#align equiv.mul_one_class Equiv.mulOneClass
#align equiv.add_zero_class Equiv.addZeroClass

@[to_additive]
noncomputable instance [Small.{v} α] [MulOneClass α] : MulOneClass (Shrink.{v} α) :=
(equivShrink α).symm.mulOneClass

Expand Down

0 comments on commit 366a5f2

Please sign in to comment.