Theorems · Theorem · nonassociative algebras

LieIdeal.isSolvable_of_killingForm_apply_lie_eq_zero

∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [CharZero R] [IsDomain R] [inst_3 : LieRing L]
  [inst_4 : LieAlgebra R L] [IsNoetherian R L] [Module.Free R L] (I : LieIdeal R L),
  (∀ x ∈ I, ∀ y ∈ ⁅I, I⁆, ((killingForm R L) x) y = 0) → LieAlgebra.IsSolvable ↥I

A convenience variation of LieAlgebra.isSolvable_of_forall_derived_killingForm_eq_zero for working with ideals. Over a principal ideal domain by LieIdeal.killingForm_eq this is just a specialisation of LieAlgebra.isSolvable_of_killingForm_apply_lie_eq_zero but since it does not require the PID assumption, it is a slightly stronger result.

Defined in

Mathlib.Algebra.Lie.CartanCriterion

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingCharZeroIsDomainLieRingLieAlgebraIsNoetherianModule.Free