Theorems · Theorem · linear algebra

LinearMap.IsIdempotentElem.range_mem_invtSubmodule

∀ {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 ∘ₗ T ∘ₗ f = T ∘ₗ f → f.range ∈ Module.End.invtSubmodule T

Alias of the reverse direction of LinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff. 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

0 results in Mathlib

Foundations

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

Assumes

RingAddCommGroupModule