Theorem LinearMap.IsProj.submodule_eq_top_iff

Modification history

2025-07-11 13:07
Mathlib/LinearAlgebra/Projection.lean
feat(LinearAlgebra/Projection): add lemmas for linear projections (#26792) …
Added LinearMap.IsProj.submodule_eq_top_iffView on Github →