Theorem LinearMap.IsProj.submodule_unique

Modification history

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