ker_mem_invtSubmodule_iff — Mathlib

English

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

Русский

Для идемпотентного f ядро f инвариантно относительно T тогда и только тогда, когда f ∘ T ∘ f = f ∘ T.

LaTeX

$$$ \ker f \in \operatorname{End}_{\!\!\!} \text{invtSubmodule}_T \iff f \circ T \circ f = f \circ T$$$

Lean4

/-- `ker f` is invariant under `T` if and only if `f ∘ₗ T ∘ₗ f = f ∘ₗ T`,
for idempotent `f`. -/
theorem ker_mem_invtSubmodule_iff (hf : IsIdempotentElem f) :
    ker f ∈ Module.End.invtSubmodule T ↔ f ∘ₗ T ∘ₗ f = f ∘ₗ T := by
  rw [← comp_assoc, hf.comp_eq_left_iff, ker_comp, Module.End.mem_invtSubmodule]

Похожие утверждения