Theorem AddEquiv.coe_toIntLinearEquiv

Modification history

2025-12-18 07:31
Mathlib/Algebra/Module/Equiv/Basic.lean
chore(Algebra/Module): make select `Module` assumptions (#32435) …
Modified AddEquiv.coe_toIntLinearEquivView on Github →
2023-01-27 06:03
Mathlib/Algebra/Module/Equiv.lean
feat : port Algebra.Module.Equiv (#1732)
Added AddEquiv.coe_toIntLinearEquivView on Github →