Theorem MulEquiv.toFun_eq_coe

Modification history

2025-01-15 21:51
Mathlib/Algebra/Group/Equiv/Basic.lean
chore(Algebra/Group/Equiv): split into `Defs` and `Basic` (#20712) …
Modified MulEquiv.toFun_eq_coeView on Github →
2025-01-13 17:00
Mathlib/Algebra/Group/Equiv/Basic.lean
chore: address some porting notes about coercions of equivs (#20714) …
Added MulEquiv.toFun_eq_coeView on Github →