Theorem LinearMap.IsIdempotentElem.range_eq_ker_one_sub

Modification history

2026-01-02 15:12
Mathlib/LinearAlgebra/Projection.lean
chore(Topology/Algebra/Module/LinearMap): deprecate duplicate lemmas (#33341) …
Added LinearMap.IsIdempotentElem.range_eq_ker_one_subView on Github →