Theorem LinearMap.ltoFun_apply

Modification history

2025-11-24 20:52
Mathlib/Algebra/Module/LinearMap/Basic.lean
chore: state `LinearMap.ltoFun` in the correct generality (#31952)
Added LinearMap.ltoFun_applyView on Github →