Theorem AlgEquiv.coe_toEquiv

Modification history

2025-01-13 17:00
Mathlib/Algebra/Algebra/Equiv.lean
chore: address some porting notes about coercions of equivs (#20714) …
Added AlgEquiv.coe_toEquivView on Github →