Theorems · Inductive type · nonassociative algebras

LieAlgebra.IsKilling

(R : Type u_1) → (L : Type u_3) → [inst : CommRing R] → [inst_1 : LieRing L] → [LieAlgebra R L] → Prop

We say a Lie algebra is Killing if its Killing form is non-singular. NB: This is not standard terminology (the literature does not seem to name Lie algebras with this property).

Defined in

Mathlib.Algebra.Lie.Killing

Cited by

122 results in Mathlib

Foundations

Depth 2 from the axioms, rests on 4 definitions · uses no axioms

Assumes

CommRingLieRingLieAlgebra