English
If an invariant submodule q is nontrivial and closed under root reflections, then q equals the top submodule.
Русский
Если инвариантное подполье не тривиально и замкнуто относительно отражений корня, то q совпадает с верхним подпольем.
LaTeX
$$$ q \\neq ⊥ \\Rightarrow q = ⊤ \\text{ under invariance assumptions }$$
Lean4
instance : (rootSystem H).IsIrreducible :=
by
have _i := nontrivial_of_isIrreducible K L L
exact RootPairing.IsIrreducible.mk' (rootSystem H).toRootPairing <| eq_top_of_invtSubmodule_ne_bot
