Commit 2024-06-04 13:47 277e3953

View on Github →

feat: simp lemma replacing MulEquiv.toMonoidHom with coercion (#13379) I was surprised to encounter post-simp goals that included both x.toMonoidHom and the coercion. I think it would be good to follow up by avoiding toMonoidHom in favour of the coercion in the first place.

Estimated changes

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

added theorem MulEquiv.toMonoidHom_eq_coe

Modified Mathlib/Algebra/Group/Submonoid/Operations.lean

modified def MulEquiv.submonoidMap

modified theorem Submonoid.map_equiv_top

modified theorem Submonoid.topEquiv_toMonoidHom

Modified Mathlib/Data/Finsupp/Basic.lean