Commit 2023-06-29 05:58 d5ecb6d7

View on Github →

feat: add MulEquiv.toMulHom_eq_coe to normalize coercions (#5546) There will probably be simpNF problems, waiting for CI.

Estimated changes

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

added theorem MulEquiv.toMulHom_eq_coe

Modified Mathlib/GroupTheory/Subsemigroup/Operations.lean

modified def MulEquiv.subsemigroupMap

modified theorem Subsemigroup.map_equiv_top