Commit 2023-06-08 17:35 ac5fb5cc

View on Github →

feat: port Algebra.Lie.Free (#4863)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Lie/Free.lean

added theorem FreeLieAlgebra.Rel.addLeft

added theorem FreeLieAlgebra.Rel.neg

added theorem FreeLieAlgebra.Rel.smulOfTower

added theorem FreeLieAlgebra.Rel.subLeft

added theorem FreeLieAlgebra.Rel.subRight

added inductive FreeLieAlgebra.Rel

added theorem FreeLieAlgebra.hom_ext

added def FreeLieAlgebra.lift

added def FreeLieAlgebra.liftAux

added theorem FreeLieAlgebra.liftAux_map_add

added theorem FreeLieAlgebra.liftAux_map_mul

added theorem FreeLieAlgebra.liftAux_map_smul

added theorem FreeLieAlgebra.liftAux_spec

added theorem FreeLieAlgebra.lift_comp_of

added theorem FreeLieAlgebra.lift_of_apply

added theorem FreeLieAlgebra.lift_symm_apply

added theorem FreeLieAlgebra.lift_unique

added def FreeLieAlgebra.mk

added def FreeLieAlgebra.of

added theorem FreeLieAlgebra.of_comp_lift

added def FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra

added def FreeLieAlgebra