range_mem_invtSubmodule_iff — Mathlib

English

The image of f is invariant under T if and only if f ∘ T ∘ f = T ∘ f, for an idempotent f.

Русский

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

LaTeX

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

Lean4

/-- `range f` is invariant under `T` if and only if `f ∘ₗ T ∘ₗ f = T ∘ₗ f`,
for idempotent `f`. -/
theorem range_mem_invtSubmodule_iff (hf : IsIdempotentElem f) :
    range f ∈ Module.End.invtSubmodule T ↔ f ∘ₗ T ∘ₗ f = T ∘ₗ f := by
  rw [hf.comp_eq_right_iff, range_comp, Module.End.mem_invtSubmodule_iff_map_le]

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