Commit 2023-09-12 12:40 2bffb702

View on Github →

chore: replace anonymous morphism constructors with named fields (#7015) This makes it easier to refactor the order or inheritance structure of morphisms without having to change all of the anonymous constructors. This is far from exhaustive.

Estimated changes

Modified Mathlib/Algebra/Category/GroupCat/Basic.lean

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

Modified Mathlib/Algebra/Category/Ring/Limits.lean

Modified Mathlib/Algebra/Free.lean

modified def Magma.AssocQuotient.of

Modified Mathlib/Algebra/Hom/Units.lean

modified def Units.coeHom

Modified Mathlib/Algebra/Lie/Basic.lean

Modified Mathlib/Algebra/Order/AbsoluteValue.lean

modified def IsAbsoluteValue.abvHom'

Modified Mathlib/Algebra/Order/Interval.lean

Modified Mathlib/Algebra/Ring/Basic.lean

modified def AddHom.mulLeft

modified def AddHom.mulRight

Modified Mathlib/Data/Finset/Pointwise.lean

modified def Finset.singletonMulHom

modified def Finset.singletonOneHom

Modified Mathlib/Data/Set/Pointwise/Basic.lean

Modified Mathlib/GroupTheory/GroupAction/Quotient.lean

modified def MulActionHom.toQuotient

Modified Mathlib/GroupTheory/GroupAction/SubMulAction.lean

Modified Mathlib/GroupTheory/Perm/Basic.lean

Modified Mathlib/GroupTheory/Subgroup/Basic.lean

Modified Mathlib/GroupTheory/Submonoid/Operations.lean

modified def Submonoid.subtype

modified def SubmonoidClass.subtype

Modified Mathlib/GroupTheory/Subsemigroup/Operations.lean

modified def MulMemClass.subtype

Modified Mathlib/Order/Filter/Germ.lean

modified def Filter.Germ.coeMulHom

Modified Mathlib/Order/Filter/Pointwise.lean

modified def Filter.pureMulHom

modified def Filter.pureOneHom

Modified Mathlib/SetTheory/Cardinal/Basic.lean

modified def Cardinal.toNat

Modified Mathlib/Topology/Algebra/Monoid.lean