Theorems · Theorem · linear algebra

LinearMap.IsIdempotentElem.comp_eq_right_iff

∀ {S : Type u_5} [inst : Semiring S] {M : Type u_6} [inst_1 : AddCommMonoid M] [inst_2 : Module S M] {q : M →ₗ[S] M},
  IsIdempotentElem q →
    ∀ {E : Type u_7} [inst_3 : AddCommMonoid E] [inst_4 : Module S E] (p : E →ₗ[S] M), q ∘ₗ p = p ↔ p.range ≤ q.range

Given an idempotent linear operator q, we have q ∘ p = p iff range p ⊆ range q for all p.

Defined in

Mathlib.LinearAlgebra.Projection

Cited by

2 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModuleAddCommMonoidModule