Mathlib v3 is deprecated. Go to Mathlib v4

Theorem alg_hom.to_lie_hom_comp

Modification history

2021-07-05 09:56

src/algebra/lie/of_associative.lean

feat(algebra/lie/free): the universal enveloping algebra of the free Lie algebra is the free associative algebra (#8183)

Added alg_hom.to_lie_hom_comp View on Github →