Theorems · Theorem · nonassociative algebras

LieModule.exists_nontrivial_weightSpace_of_isNilpotent

∀ (k : Type u_1) (L : Type u_3) (M : Type u_4) [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M]
  [inst_3 : LieRing.IsNilpotent L] [inst_4 : Field k] [inst_5 : LieAlgebra k L] [inst_6 : Module k M]
  [Module.Finite k M] [inst_8 : LieModule k L M] [LieModule.LinearWeights k L M] [LieModule.IsTriangularizable k L M]
  [Nontrivial M], ∃ χ, Nontrivial ↥(LieModule.weightSpace M ⇑χ)

See LieModule.exists_nontrivial_weightSpace_of_isSolvable for the variant that only assumes that L is solvable but additionally requires k to be of characteristic zero.

Defined in

Mathlib.Algebra.Lie.Weights.Linear

Cited by

0 results in Mathlib

Foundations

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

Assumes

LieRingAddCommGroupLieRingModuleLieRing.IsNilpotentFieldLieAlgebraModuleModule.FiniteLieModuleLieModule.LinearWeightsLieModule.IsTriangularizableNontrivial