Commit 2024-08-09 14:59 4d65f9eb

View on Github →

perf: to_additive (attr := reducible) -> abbrev (#15476)

Estimated changes

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

deleted def Function.Surjective.mulActionLeft

deleted def MulAction.compHom

deleted def SMul.comp

Modified Mathlib/Algebra/Group/InjSurj.lean

Modified Mathlib/Algebra/Group/MinimalAxioms.lean

deleted def Group.ofLeftAxioms

deleted def Group.ofRightAxioms

Modified Mathlib/Algebra/Order/Group/InjSurj.lean

deleted def Function.Injective.linearOrderedCommGroup

deleted def Function.Injective.orderedCommGroup

Modified Mathlib/Algebra/Order/Monoid/Basic.lean

deleted def Function.Injective.linearOrderedCancelCommMonoid

deleted def Function.Injective.linearOrderedCommMonoid

deleted def Function.Injective.orderedCancelCommMonoid

deleted def Function.Injective.orderedCommMonoid

Modified Mathlib/Analysis/Normed/Group/Basic.lean

deleted def GroupNorm.toNormedCommGroup

deleted def GroupNorm.toNormedGroup

deleted def GroupSeminorm.toSeminormedCommGroup

deleted def GroupSeminorm.toSeminormedGroup

deleted def NormedCommGroup.induced

deleted def NormedCommGroup.ofMulDist'

deleted def NormedCommGroup.ofMulDist

deleted def NormedCommGroup.ofSeparation

deleted def NormedGroup.induced

deleted def NormedGroup.ofMulDist'

deleted def NormedGroup.ofMulDist

deleted def NormedGroup.ofSeparation

deleted def SeminormedCommGroup.induced

deleted def SeminormedCommGroup.ofMulDist'

deleted def SeminormedCommGroup.ofMulDist

deleted def SeminormedGroup.induced

deleted def SeminormedGroup.ofMulDist'

deleted def SeminormedGroup.ofMulDist

Modified Mathlib/GroupTheory/EckmannHilton.lean

deleted def EckmannHilton.commGroup

deleted def EckmannHilton.commMonoid

Modified Mathlib/GroupTheory/Exponent.lean

deleted def commMonoidOfExponentTwo

Modified Mathlib/GroupTheory/GroupAction/Basic.lean

deleted def MulAction.orbitRel.Quotient

Modified Mathlib/GroupTheory/MonoidLocalization/Basic.lean

deleted def Localization.Away.monoidOf

deleted def Localization.Away

deleted def Submonoid.LocalizationMap.AwayMap

Modified Mathlib/GroupTheory/SpecificGroups/KleinFour.lean

deleted def IsKleinFour.mulEquiv

Modified Mathlib/Logic/Equiv/TransferInstance.lean

Modified Mathlib/MeasureTheory/Measure/Haar/Basic.lean