Theorems · Theorem · nonassociative algebras

RootPairing.eq_top_of_mem_invtSubmodule_of_forall_eq_univ

∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] {K : Type u_5}
  [inst_2 : Field K] [NeZero 2] [inst_4 : Module K M] [inst_5 : Module K N] (P : RootPairing ι K M N) [P.IsRootSystem]
  (q : Submodule K M),
  q ≠ ⊥ →
    (∀ (i : ι), q ∈ Module.End.invtSubmodule ↑(P.reflection i)) →
      (∀ (Φ : Set ι), Φ.Nonempty → ⇑P.root '' Φ ⊆ ↑q → (∀ i ∉ Φ, q ≤ LinearMap.ker (P.coroot' i)) → Φ = Set.univ) →
        q = ⊤

Defined in

Mathlib.LinearAlgebra.RootSystem.Irreducible

Cited by

0 results in Mathlib

Foundations

Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroupAddCommGroupFieldNeZeroModuleModuleRootPairing.IsRootSystem