Commit 2025-05-12 07:47 bbbe0a92

View on Github →

chore: deduplicate equivalence M ≃ (ℕ →+ M) for M an additive monoid (#24783) The second versions were introduced in #11669, with no discussion. Moves:

AddMonoidHom.fromNatEquiv → multiplesHom
AddMonoidHom.fromULiftNatEquiv → uliftMultiplesHom
AddMonoidHom.fromIntEquiv → zmultiplesHom
AddMonoidHom.fromULiftIntEquiv → uliftZMultiplesHom
MonoidHom.fromMultiplicativeNatEquiv → powersHom
MonoidHom.fromULiftMultiplicativeNatEquiv → uliftPowersHom
MonoidHom.fromMultiplicativeIntEquiv → zpowersHom
MonoidHom.fromULiftMultiplicativeIntEquiv → uliftZPowersHom

Estimated changes

Modified Mathlib/Algebra/Category/Grp/ForgetCorepresentable.lean

modified def AddMonoidHom.fromIntEquiv

modified def MonoidHom.fromMultiplicativeIntEquiv

added def uliftZMultiplesHom

added def uliftZPowersHom

Modified Mathlib/Algebra/Category/MonCat/ForgetCorepresentable.lean

modified def AddMonoidHom.fromNatEquiv

modified def MonoidHom.fromMultiplicativeNatEquiv

added def uliftMultiplesHom

added def uliftPowersHom

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