We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 00ec302 commit e688ba0Copy full SHA for e688ba0
1 file changed
Mathlib/RingTheory/Bialgebra/Primitive.lean
@@ -23,7 +23,7 @@ This file defines primitive elements in a bialgebra, i.e. elements `a` such that
23
* `primitiveSubmodule` is a `LieSubalgebra` with bracket `[a, b] = a * b - b * a`.
24
(`IsPrimitiveElem.commutator` is stated with `a * b - b * a` rather than `⁅a, b⁆` to avoid
25
importing Lie theory into this file.)
26
-* (Cartier–Milnor–Moore) In characteristic 0 over a field, the primitive elements of a
+* (Milnor–Moore) In characteristic 0 over a field, the primitive elements of a
27
cocommutative connected bialgebra generate it as the universal enveloping of a Lie algebra.
28
* Generalize to `(g, h)`-skew-primitive elements `Δ a = a ⊗ₜ g + h ⊗ₜ a` for group-like `g`, `h`
29
over a plain coalgebra, of which primitivity is the `(1, 1)` case over a bialgebra.
0 commit comments