Theorems · Definition · nonassociative algebras

LieDerivation.exp

{R : Type u_1} →
  {L : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra R L] → [LieAlgebra ℚ L] → (D : LieDerivation R L L) → IsNilpotent ↑D → L ≃ₗ⁅R⁆ L

In characteristic zero, the exponential of a nilpotent derivation is a Lie algebra automorphism.

Defined in

Mathlib.Algebra.Lie.Derivation.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingLieRingLieAlgebraLieAlgebra