Commit 2024-04-29 08:00 0a97fb7a

View on Github →

chore: Move monoid with zero instances on pi types (#12286) Move everything that can't be additivised out of Algebra.Group.Pi.Lemmas:

MulZeroClass, MulZeroOneClass, etc... instances go to a new Algebra.GroupWithZero.Pi file. I credit Eric W. for https://github.com/leanprover-community/mathlib/pull/4766.
AddMonoidWithOne, AddGroupWithOne instances go to Algebra.Ring.Pi.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Hom/End.lean

added theorem AddMonoid.End.natCast_apply

added theorem AddMonoid.End.ofNat_apply

Modified Mathlib/Algebra/Group/Hom/Instances.lean

deleted theorem AddMonoid.End.natCast_apply

deleted theorem AddMonoid.End.ofNat_apply

Modified Mathlib/Algebra/Group/Pi/Lemmas.lean

deleted def MulHom.single

deleted theorem Pi.single_mul

deleted theorem Pi.single_mul_left

deleted theorem Pi.single_mul_left_apply

deleted theorem Pi.single_mul_right

deleted theorem Pi.single_mul_right_apply

Created Mathlib/Algebra/GroupWithZero/Pi.lean

added def MulHom.single

added theorem Pi.single_mul

added theorem Pi.single_mul_left

added theorem Pi.single_mul_left_apply

added theorem Pi.single_mul_right

added theorem Pi.single_mul_right_apply

Modified Mathlib/Algebra/Ring/Pi.lean