Theorem LinearMap.IsIdempotentElem.comp_eq_right_iff

Modification history

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