Theorems · Definition · nonassociative algebras

LieIdeal

(R : Type u) → (L : Type v) → [inst : CommRing R] → [inst_1 : LieRing L] → [LieAlgebra R L] → Type v

An ideal of a Lie algebra is a Lie submodule of the Lie algebra as a Lie module over itself.

Defined in

Mathlib.Algebra.Lie.Ideal

Cited by

282 results in Mathlib

Foundations

Depth 8 from the axioms, rests on 57 definitions · uses no axioms

Assumes

CommRingLieRingLieAlgebra