Commit 2023-06-08 09:01 4c891470

View on Github →

feat: port Algebra.Lie.UniversalEnveloping (#4827)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Lie/UniversalEnveloping.lean

added inductive UniversalEnvelopingAlgebra.Rel

added theorem UniversalEnvelopingAlgebra.hom_ext

added def UniversalEnvelopingAlgebra.lift

added theorem UniversalEnvelopingAlgebra.lift_symm_apply

added theorem UniversalEnvelopingAlgebra.lift_unique

added theorem UniversalEnvelopingAlgebra.lift_ι_apply'

added theorem UniversalEnvelopingAlgebra.lift_ι_apply

added def UniversalEnvelopingAlgebra.mkAlgHom

added def UniversalEnvelopingAlgebra.ι

added theorem UniversalEnvelopingAlgebra.ι_comp_lift

added def UniversalEnvelopingAlgebra