Commit 2022-12-22 21:16 e8655308

View on Github →

feat: better coercions from hom classes to hom types (#1150) Discussed here

Estimated changes

Modified Mathlib/Algebra/Hom/Equiv/Basic.lean

added def MulEquivClass.toMulEquiv

Modified Mathlib/Algebra/Hom/Group.lean

added def MonoidHomClass.toMonoidHom

added def MonoidWithZeroHomClass.toMonoidWithZeroHom

added def MulHomClass.toMulHom

added def OneHomClass.toOneHom

Modified Mathlib/Algebra/Hom/Ring.lean

added def NonUnitalRingHomClass.toNonUnitalRingHom

modified theorem RingHom.toMonoidWithZeroHom_eq_coe

added def RingHomClass.toRingHom

Modified Mathlib/Logic/Equiv/Defs.lean

added def EquivLike.toEquiv

Modified Mathlib/Order/Hom/Basic.lean

added def OrderHomClass.toOrderHom

added def OrderIsoClass.toOrderIso