Theorem LinearMap.IsProj.subtype_comp_codRestrict

Modification history

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