Theorem LinearEquiv.coe_ofLinearMap

Modification history

2026-08-03 21:26
Mathlib/Algebra/Module/Equiv/Basic.lean
refactor(Algebra/Module/Equiv): update name and refactor API ofLinearEquiv (#40865) …
Added LinearEquiv.coe_ofLinearMapView on Github →