Theorems · Theorem · nonassociative algebras

LieAlgebra.hasCentralRadical_and_of_isIrreducible_of_isFaithful

∀ (k : Type u_1) (L : Type u_2) (M : Type u_3) [inst : Field k] [CharZero k] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra k L] [Module.Finite k L] [inst_5 : AddCommGroup M] [inst_6 : Module k M]
  [inst_7 : LieRingModule L M] [inst_8 : LieModule k L M] [Module.Finite k M] [LieModule.IsIrreducible k L M]
  [LieModule.IsFaithful k L M] [LieModule.IsTriangularizable k L M],
  LieAlgebra.HasCentralRadical k L ∧ ∀ (x : L), x ∈ LieAlgebra.center k L ↔ (LieModule.toEnd k L M) x ∈ k ∙ LinearMap.id

Defined in

Mathlib.Algebra.Lie.Semisimple.Lemmas

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldCharZeroLieRingLieAlgebraModule.FiniteAddCommGroupModuleLieRingModuleLieModuleModule.FiniteLieModule.IsIrreducibleLieModule.IsFaithfulLieModule.IsTriangularizable