Theorem LinearMap.IsProj.isIdempotentElem

Modification history

2025-07-11 13:07

Mathlib/LinearAlgebra/Projection.lean

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

Added LinearMap.IsProj.isIdempotentElem View on Github →