Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-01 12:58 3fa61ea4

View on Github →

feat(algebra/lie/free): construction of free Lie algebras (#8153)

Estimated changes

Created src/algebra/lie/free.lean

added theorem free_lie_algebra.hom_ext

added def free_lie_algebra.lift

added def free_lie_algebra.lift_aux

added theorem free_lie_algebra.lift_aux_map_add

added theorem free_lie_algebra.lift_aux_map_mul

added theorem free_lie_algebra.lift_aux_map_smul

added theorem free_lie_algebra.lift_aux_spec

added theorem free_lie_algebra.lift_comp_of

added theorem free_lie_algebra.lift_of_apply

added theorem free_lie_algebra.lift_symm_apply

added theorem free_lie_algebra.lift_unique

added def free_lie_algebra.mk

added def free_lie_algebra.of

added theorem free_lie_algebra.of_comp_lift

added theorem free_lie_algebra.rel.add_left

added inductive free_lie_algebra.rel

added def free_lie_algebra

Created src/algebra/lie/non_unital_non_assoc_algebra.lean

added def lie_hom.to_non_unital_alg_hom

added def lie_ring.to_non_unital_non_assoc_semiring

Modified src/algebra/non_unital_alg_hom.lean

added theorem non_unital_alg_hom.congr_fun