Commit 2026-09-10 14:29 1f5affdb
View on Github →chore(Algebra/Group/Equiv/TypeTags): generalize to Add and Mul and deprecate duplicates (#43661)
This PR generalizes some of the defs in Algebra/Group/Equiv/TypeTags.lean to Add and Mul and deprecates some duplicate declarations.
(You can check that I got all of the multiplicative/additive maps right by writing attribute [local irreducible] Additive Multiplicative at the top of the file)
Deprecations:
- monoidEndToAdditive
- monoidEndToAdditive_apply_apply
- monoidEndToAdditive_symm_apply_apply
- addMonoidEndToMultiplicative
- addMonoidEndToMultiplicative_apply_apply
- addMonoidEndToMultiplicative_symm_apply_apply
- MulEquiv.Monoid.End
- MulEquiv.Monoid.End_apply_apply
- MulEquiv.Monoid.End_symm_apply_apply
- MulEquiv.AddMonoid.End
- MulEquiv.AddMonoid.End_apply_apply
- MulEquiv.AddMonoid.End_symm_apply_apply
- MulEquiv.toMultiplicative_toAdditive
- MulEquiv.toMultiplicative_toAdditive_apply
- MulEquiv.toMultiplicative_toAdditive_symm_apply
- AddEquiv.toAdditive_toMultiplicative
- AddEquiv.toAdditive_toMultiplicative_apply
- AddEquiv.toAdditive_toMultiplicative_symm_apply