Theorems · Definition · nonassociative algebras

LieAlgebra.rank

(R : Type u_1) →
  (L : Type u_3) →
    [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → [Module.Finite R L] → [Module.Free R L] → ℕ

Let L be a Lie algebra over a nontrivial commutative ring R, and assume that L is finite free as R-module. Then the coefficients of the characteristic polynomial of ad R L x are polynomial in x. The rank of L is the smallest n for which the n-th coefficient is not the zero polynomial.

Defined in

Mathlib.Algebra.Lie.Rank

Cited by

10 results in Mathlib

Foundations

Depth 109 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingLieRingLieAlgebraModule.FiniteModule.Free