Theorem LinearMap.isProj_range_iff_isIdempotentElem

Modification history

2025-07-11 13:07

Mathlib/LinearAlgebra/Projection.lean

feat(LinearAlgebra/Projection): add lemmas for linear projections (#26792) …

Added LinearMap.isProj_range_iff_isIdempotentElem View on Github →