Theorems · Definition · nonassociative algebras

LieAlgebra.LieCharacter

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

A character of a Lie algebra is a morphism to the scalars.

Defined in

Mathlib.Algebra.Lie.Character

Cited by

5 results in Mathlib

Foundations

Depth 43 from the axioms · uses propext, Quot.sound

Assumes

CommRingLieRingLieAlgebra