Def LinearEquiv.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.ofLinearMap View on Github →