Commit 2023-01-16 20:07 9b5ec8ff

View on Github →

feat: add HomClass.toHom coercions to Algebra.Order.Hom.Monoid (#1603) To create good coercion behaviour for the Homs and fix some broken norm_casts in #1482, added OrderMonoidHomClass.toOrderMonoidHom and OrderMonoidWithZeroHomClass.toOrderMonoidWithZeroHom to Algebra.Order.Hom.Monoid. This is consistent with how we have been treating coercions of Homs in other files recently, such as Algebra.Hom.GroupAction. Also golfed some ext; rfls in that file to rfls since that now works.

Estimated changes

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

modified theorem OrderMonoidHom.comp_mul

modified theorem OrderMonoidHom.comp_one

modified theorem OrderMonoidHom.toMonoidHom_eq_coe

modified theorem OrderMonoidHom.toOrderHom_eq_coe

added def OrderMonoidHomClass.toOrderMonoidHom

modified theorem OrderMonoidWithZeroHom.comp_id

modified theorem OrderMonoidWithZeroHom.id_comp

modified theorem OrderMonoidWithZeroHom.mk_coe

added def OrderMonoidWithZeroHomClass.toOrderMonoidWithZeroHom