Def LinearMap.leftInverse

Modification history

2025-11-21 04:24
Mathlib/LinearAlgebra/Basis/VectorSpace.lean
chore: make `CLM.extend` total and define `LM.leftInverse` (#31799) …
Added LinearMap.leftInverseView on Github →