Theorems · Inductive type · nonassociative algebras

GradedLieAlgebra

{ι : Type u_1} →
  {R : Type u_3} →
    {L : Type u_4} →
      [DecidableEq ι] →
        [AddCommMonoid ι] →
          [inst : CommRing R] →
            [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → (ι → Submodule R L) → Type (max u_1 u_4)

A class that ensures a Lie algebra has a bracket that preserves a decomposition.

Defined in

Mathlib.Algebra.Lie.Graded

Cited by

5 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

DecidableEqAddCommMonoidCommRingLieRingLieAlgebra