Theorems · Inductive type · nonassociative algebras

LieAlgebra.Basis

(ι : Type u_1) →
  {R : Type u_2} →
    {L : Type u_3} →
      [Finite ι] →
        [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → LieSubalgebra R L → Type (max u_1 u_3)

A basis for a semisimple Lie algebra distinguishes a natural Cartan subalgebra and a base for the associated root system.

Defined in

Mathlib.Algebra.Lie.Basis.Basic

Cited by

44 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

FiniteCommRingLieRingLieAlgebra