Theorems · Theorem · nonassociative algebras

LieModule.exists_nontrivial_weightSpace_of_lieIdeal

∀ {k : Type u_1} [inst : Field k] {L : Type u_2} [inst_1 : LieRing L] [inst_2 : LieAlgebra k L] {V : Type u_3}
  [inst_3 : AddCommGroup V] [inst_4 : Module k V] [inst_5 : LieRingModule L V] [inst_6 : LieModule k L V] [CharZero k]
  [Module.Finite k V] [LieModule.IsTriangularizable k L V] (A : LieIdeal k L),
  IsCoatom ↑A →
    ∀ (χ₀ : Module.Dual k ↥A) [Nontrivial ↥(LieModule.weightSpace V ⇑χ₀)], ∃ χ, Nontrivial ↥(LieModule.weightSpace V ⇑χ)

Defined in

Mathlib.Algebra.Lie.LieTheorem

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldLieRingLieAlgebraAddCommGroupModuleLieRingModuleLieModuleCharZeroModule.FiniteLieModule.IsTriangularizableNontrivial