mem_invtRootSubmodule_iff — Mathlib

English

An element q is in P.invtRootSubmodule iff for every i, q lies in Module.End.invtSubmodule (P.reflection i).

Русский

Элемент q принадлежит P.invtRootSubmodule тогда и только тогда, когда для каждого i выполняется q ∈ Module.End.invtSubmodule (P.reflection i).

LaTeX

$$$$ q \in P.invtRootSubmodule \;\Longleftrightarrow\; \forall i, \ q \in Module.End.invtSubmodule (P.reflection i). $$$$

Lean4

theorem mem_invtRootSubmodule_iff {q : Submodule R M} :
    q ∈ P.invtRootSubmodule ↔ ∀ i, q ∈ Module.End.invtSubmodule (P.reflection i) := by simp [invtRootSubmodule]

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