invtRootSubmodule — Mathlib

English

If M is nontrivial, then the invariant submodule P.invtRootSubmodule is nontrivial.

Русский

Если M ненулевой, то инвариантное подпространство P.invtRootSubmodule ненулевое.

LaTeX

$$$$ M \neq \{0\} \Rightarrow \exists q \in P.invtRootSubmodule, q \neq \{0\}. $$$$

Lean4

/-- The sublattice of invariant submodules of the root space. -/
def invtRootSubmodule : Sublattice (Submodule R M) :=
  ⨅ i, invtSubmodule (P.reflection i)

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