Commit 2023-08-19 12:28 0a3c0125

View on Github →

chore: make sure that some coercions have an attached definition (#6667)

Estimated changes

Modified Mathlib/Algebra/Algebra/Equiv.lean

added def AlgEquivClass.toAlgEquiv

Modified Mathlib/Algebra/Hom/NonUnitalAlg.lean

added def NonUnitalAlgHomClass.toNonUnitalAlgHom

Modified Mathlib/Algebra/Star/StarAlgHom.lean

added def NonUnitalStarAlgHomClass.toNonUnitalStarAlgHom

added def StarAlgHomClass.toStarAlgHom

Modified Mathlib/Order/Hom/Basic.lean

Modified Mathlib/Topology/ContinuousFunction/CocompactMap.lean

added def CocompactMapClass.toCocompactMap

Modified Mathlib/Topology/Order/Hom/Basic.lean