Theorems · Theorem · linear algebra

LinearMap.IsIdempotentElem.ker_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.ker ∈ Module.End.invtSubmodule T ↔ f ∘ₗ T ∘ₗ f = f ∘ₗ T)

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

Defined in

Mathlib.LinearAlgebra.Projection

Cited by

4 results in Mathlib

Foundations

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

Assumes

RingAddCommGroupModule