Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-26 19:15 d0b59476

View on Github →

feat(algebra/universal_enveloping_algebra): construction of universal enveloping algebra and its universal property (#4041)

Main definitions

universal_enveloping_algebra
universal_enveloping_algebra.algebra
universal_enveloping_algebra.lift
universal_enveloping_algebra.ι_comp_lift
universal_enveloping_algebra.lift_unique
universal_enveloping_algebra.hom_ext

Estimated changes

Modified src/algebra/lie_algebra.lean

added theorem lie_algebra.coe_to_linear_map

added theorem lie_algebra.morphism.ext

Created src/algebra/universal_enveloping_algebra.lean

added theorem universal_enveloping_algebra.hom_ext

added def universal_enveloping_algebra.lift

added theorem universal_enveloping_algebra.lift_unique

added theorem universal_enveloping_algebra.lift_ι_apply

added def universal_enveloping_algebra.mk_alg_hom

added inductive universal_enveloping_algebra.rel

added def universal_enveloping_algebra.ι

added theorem universal_enveloping_algebra.ι_comp_lift

added def universal_enveloping_algebra

Modified src/linear_algebra/tensor_algebra.lean

Modified src/ring_theory/algebra.lean