Theorems · Theorem · nonassociative algebras

FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra_symm_apply

∀ (R : Type u) (X : Type v) [inst : CommRing R] (a : FreeAlgebra R X),
  (FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra R X).symm a =
    ((FreeAlgebra.lift R) (⇑(UniversalEnvelopingAlgebra.ι R) ∘ FreeLieAlgebra.of R)) a

Defined in

Mathlib.Algebra.Lie.Free

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRing