Mathlib Changelog
v4
Changelog
About
Github
Theorem
MulEquiv.toMulHom_eq_coe
Modification history
2023-06-29 05:58
Mathlib/Algebra/Hom/Equiv/Basic.lean
feat: add MulEquiv.toMulHom_eq_coe to normalize coercions (#5546) …
Added
MulEquiv.toMulHom_eq_coe
View on Github →