Theorem LinearMap.IsIdempotentElem.mem_range_iff

Modification history

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