Theorem MulEquiv.coe_monoidHom_trans

Modification history

2026-09-15 17:41
Mathlib/Algebra/Group/Equiv/Defs.lean
chore(Algebra/MonoidHom): rename to `.ofClass` (#43755) …
Deleted MulEquiv.coe_monoidHom_transView 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_transView on Github →
2024-02-14 08:30
Mathlib/Algebra/Group/Equiv/Basic.lean
feat(Algebra/Group): Miscellaneous lemmas (#9387) …
Modified MulEquiv.coe_monoidHom_transView on Github →
2022-12-06 23:13
Mathlib/Algebra/Hom/Equiv/Basic.lean
feat: port Algebra.Hom.Equiv.Basic (#835) …
Added MulEquiv.coe_monoidHom_transView on Github →