Theorem LinearMap.leftInverse_apply_of_inj

Modification history

2025-11-21 04:24

Mathlib/LinearAlgebra/Basis/VectorSpace.lean

chore: make `CLM.extend` total and define `LM.leftInverse` (#31799) …

Added LinearMap.leftInverse_apply_of_inj View on Github →