Theorems · Definition · nonassociative algebras
UniversalEnvelopingAlgebra
(R : Type u₁) → (L : Type u₂) → [inst : CommRing R] → [inst_1 : LieRing L] → [LieAlgebra R L] → Type (max u₁ u₂)
The universal enveloping algebra of a Lie algebra.
- Defined in
- Mathlib.Algebra.Lie.UniversalEnveloping
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 40 from the axioms · uses propext, Quot.sound
- Assumes
- CommRingLieRingLieAlgebra
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- LieRingstatement and proof · cited by 1,548
- LieAlgebrastatement and proof · cited by 1,246
- RingCon.Quotientproof · cited by 118
- UniversalEnvelopingAlgebra.ringConproof · cited by 0
Cited by14
Results whose statement or proof uses this declaration.
- UniversalEnvelopingAlgebra.ιstatement and proof · cited by 8
- UniversalEnvelopingAlgebra.liftstatement and proof · cited by 7
- UniversalEnvelopingAlgebra.mkAlgHomstatement · cited by 3
- UniversalEnvelopingAlgebra.ι_applystatement · cited by 2
- FreeLieAlgebra.universalEnvelopingEquivFreeAlgebrastatement · cited by 2
- UniversalEnvelopingAlgebra.hom_extstatement and proof · cited by 1
- UniversalEnvelopingAlgebra.lift_ι_applystatement · cited by 1
- UniversalEnvelopingAlgebra.ι_comp_liftstatement · cited by 1
- UniversalEnvelopingAlgebra.hom_ext_iffstatement and proof · cited by 0
- UniversalEnvelopingAlgebra.lift_symm_applystatement and proof · cited by 0
- UniversalEnvelopingAlgebra.lift_uniquestatement and proof · cited by 0
- UniversalEnvelopingAlgebra.lift_ι_apply'statement · cited by 0