Theorems · Theorem · linear algebra

LinearMap.IsIdempotentElem.mem_range_iff

∀ {S : Type u_5} [inst : Semiring S] {M : Type u_6} [inst_1 : AddCommMonoid M] [inst_2 : Module S M] {p : M →ₗ[S] M},
  IsIdempotentElem p → ∀ {x : M}, x ∈ p.range ↔ p x = x

Given an idempotent linear operator p, we have x ∈ range p if and only if p(x) = x for all x.

Defined in

Mathlib.LinearAlgebra.Projection

Cited by

3 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModule