Theorem LinearEquiv.coe_mk

Modification history

2025-05-02 14:15
Mathlib/Algebra/Module/Equiv/Defs.lean
fix(Module/Equiv): fix `LinearEquiv.coe_mk` (#24553) …
Modified LinearEquiv.coe_mkView on Github →
2024-07-19 02:45
Mathlib/Algebra/Module/Equiv/Basic.lean
chore: split Algebra/Module/Equiv (#14466)
Modified LinearEquiv.coe_mkView on Github →
2023-02-13 18:55
Mathlib/Algebra/Module/Equiv.lean
fix: Add back LinearEquiv.coe_mk (#2253) …
Added LinearEquiv.coe_mkView on Github →