17 Nonassociative rings and algebras

TheoremLie's theorem#

Lie's theorem: Lie modules of solvable Lie algebras over fields of characteristic 0 have a common eigenvector for the action of all elements of the Lie algebra.

See LieModule.exists_nontrivial_weightSpace_of_isNilpotent for the variant that assumes that L is nilpotent and drops the condition that k is of characteristic zero.

LieModule.exists_nontrivial_weightSpace_of_isSolvable.{u_1, u_2, u_3} (k : Type u_1) [Field k]
  (L : Type u_2) [LieRing L] [LieAlgebra k L] (V : Type u_3) [AddCommGroup V] [_root_.Module k V]
  [LieRingModule L V] [LieModule k L V] [CharZero k] [Module.Finite k V] [Nontrivial V]
  [LieAlgebra.IsSolvable L] [LieModule.IsTriangularizable k L V] :
  ∃ χ, Nontrivial ↥(LieModule.weightSpace V ⇑χ)

Sources

• Mathlib documentation: LieModule.exists_nontrivial_weightSpace_of_isSolvable
• Source of LieModule.exists_nontrivial_weightSpace_of_isSolvable in Mathlib/Algebra/Lie/LieTheorem.lean
• 1000+ theorems list: Q20971632
• 1000+ theorems project: Q20971632
• Wikipedia: Lie's theorem
• Wikidata: Q20971632

MathlibLieModule.exists_nontrivial_weightSpace_of_isSolvable

Uses 21

Statement usesAlgebra of endomorphisms of a vector space · Characteristic zero · Dual vector space · Field · Finite set · Generalized eigenspaces · Generating sets · Lie algebra · Rational number · Ring structure \(\Z\)

Proof usesBasis · Cardinal · Eigenvalue · Eigenvector · Finite-dimensionality · Linear independence · Noetherian module · Noetherian ring · Principal ideal domain · Product of vector spaces · Range of a linear map

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.