Theorem MulEquiv.coe_monoidHom_symm_comp_coe_monoidHom

Modification history

2026-09-15 17:41
Mathlib/Algebra/Group/Equiv/Defs.lean
chore(Algebra/MonoidHom): rename to `.ofClass` (#43755) …
Deleted MulEquiv.coe_monoidHom_symm_comp_coe_monoidHomView on Github →
2025-01-15 21:51
Mathlib/Algebra/Group/Equiv/Basic.lean
chore(Algebra/Group/Equiv): split into `Defs` and `Basic` (#20712) …
Modified MulEquiv.coe_monoidHom_symm_comp_coe_monoidHomView on Github →
2024-02-14 08:30
Mathlib/Algebra/Group/Equiv/Basic.lean
feat(Algebra/Group): Miscellaneous lemmas (#9387) …
Added MulEquiv.coe_monoidHom_symm_comp_coe_monoidHomView on Github →