Theorems · Theorem · linear algebra

LinearMap.IsIdempotentElem.eq_projection

∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {T : E →ₗ[R] E}
  (hT : IsIdempotentElem T), T = T.range.projection T.ker ⋯

An idempotent linear operator is equal to the linear projection onto its range along its kernel.

Defined in

Mathlib.LinearAlgebra.Projection

Cited by

5 results in Mathlib

Foundations

Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingAddCommGroupModule