Theorems · Definition · nonassociative algebras

LieIdeal.rootSet

{K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra K L] →
          [inst_3 : FiniteDimensional K L] →
            {H : LieSubalgebra K L} → [inst_4 : H.IsCartanSubalgebra] → LieIdeal K L → Set ↥LieSubalgebra.root

The set of roots whose root space is contained in a given Lie ideal.

Defined in

Mathlib.Algebra.Lie.Weights.IsSimple

Cited by

10 results in Mathlib

Foundations

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

Assumes

FieldLieRingLieAlgebraFiniteDimensionalLieSubalgebra.IsCartanSubalgebra