Commit 2025-10-08 17:24 3c8f6c9a

View on Github →

chore: rename MonoidHom.toAdditive'' to MonoidHom.toAdditiveLeft (#29800) and alike

Estimated changes

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

modified def AddAction.toPermHom

Modified Mathlib/Algebra/Group/Equiv/TypeTags.lean

deleted def AddEquiv.toMultiplicative''

deleted def AddEquiv.toMultiplicative'

added def AddEquiv.toMultiplicativeLeft

added def AddEquiv.toMultiplicativeRight

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

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

deleted theorem AddMonoidHom.coe_toMultiplicative''

deleted theorem AddMonoidHom.coe_toMultiplicative'

added theorem AddMonoidHom.coe_toMultiplicativeLeft

added theorem AddMonoidHom.coe_toMultiplicativeRight

deleted def AddMonoidHom.toMultiplicative''

deleted def AddMonoidHom.toMultiplicative'

added def AddMonoidHom.toMultiplicativeLeft

added def AddMonoidHom.toMultiplicativeRight

deleted theorem MonoidHom.coe_toAdditive''

deleted theorem MonoidHom.coe_toAdditive'

added theorem MonoidHom.coe_toAdditiveLeft

added theorem MonoidHom.coe_toAdditiveRight

deleted def MonoidHom.toAdditive''

deleted def MonoidHom.toAdditive'

added def MonoidHom.toAdditiveLeft

added def MonoidHom.toAdditiveRight

Modified Mathlib/Algebra/Order/Hom/TypeTags.lean

deleted def OrderAddMonoidIso.toMultiplicative''

deleted def OrderAddMonoidIso.toMultiplicative'

added def OrderAddMonoidIso.toMultiplicativeLeft

added def OrderAddMonoidIso.toMultiplicativeRight

Modified Mathlib/Data/Finsupp/Ext.lean

Modified Mathlib/Data/Int/Cast/Lemmas.lean

Modified Mathlib/FieldTheory/KummerExtension.lean

Modified Mathlib/GroupTheory/ArchimedeanDensely.lean

Modified Mathlib/GroupTheory/FiniteAbelian/Basic.lean

Modified Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean

Modified Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean

Modified Mathlib/RingTheory/FreeCommRing.lean

Modified Mathlib/RingTheory/Valuation/RankOne.lean