Theorems · Theorem · linear algebra

LinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff

∀ {E : Type u_1} {R : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup E] [inst_2 : Module R E] {T f : E →ₗ[R] E},
  IsIdempotentElem f → (f.range ∈ Module.End.invtSubmodule T ↔ f ∘ₗ T ∘ₗ f = T ∘ₗ f)

range f is invariant under T if and only if f ∘ₗ T ∘ₗ f = T ∘ₗ f, for idempotent f.

Defined in

Mathlib.LinearAlgebra.Projection

Cited by

5 results in Mathlib

Foundations

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

Assumes

RingAddCommGroupModule