Theorem LinearEquiv.toLinearMap_ofLinearMap

Modification history

2026-08-05 02:09
Mathlib/Algebra/Module/Equiv/Basic.lean
chore(Algebra/Module/Equiv/Basic): fix lemma name (#42441)
Added LinearEquiv.toLinearMap_ofLinearMapView on Github →