Diff — Universal enveloping algebra

Revision #2471 → #3102 · back to history

addedU(g) is always infinite-dimensional68d5969534a8

addedU(g) as tensor algebra modulo two-sided ideal0ad887b2c82e

addedCanonical embedding ι: g → U(g)6f66dd93df49

modifiedKronecker product isomorphism385a74759caa

Field	From #2471	To #3102
note	No Hopf-algebra comultiplication/Kronecker product on `UniversalEnvelopingAlgebra` is defined in Mathlib.	No U(g₁ ⊕ g₂) ≅ U(g₁) ⊗ U(g₂) isomorphism on `UniversalEnvelopingAlgebra` is defined in Mathlib.