diff --git a/Mathlib.lean b/Mathlib.lean
index 1db92a61911933..223f9c39caa49e 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -6487,6 +6487,7 @@ public import Mathlib.RingTheory.Bialgebra.Equiv
 public import Mathlib.RingTheory.Bialgebra.GroupLike
 public import Mathlib.RingTheory.Bialgebra.Hom
 public import Mathlib.RingTheory.Bialgebra.MonoidAlgebra
+public import Mathlib.RingTheory.Bialgebra.Primitive
 public import Mathlib.RingTheory.Bialgebra.Quotient
 public import Mathlib.RingTheory.Bialgebra.SymmetricAlgebra
 public import Mathlib.RingTheory.Bialgebra.TensorProduct
@@ -6648,8 +6649,10 @@ public import Mathlib.RingTheory.HahnSeries.Valuation
 public import Mathlib.RingTheory.Henselian
 public import Mathlib.RingTheory.HopfAlgebra.Basic
 public import Mathlib.RingTheory.HopfAlgebra.Convolution
+public import Mathlib.RingTheory.HopfAlgebra.Generators
 public import Mathlib.RingTheory.HopfAlgebra.GroupLike
 public import Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra
+public import Mathlib.RingTheory.HopfAlgebra.Primitive
 public import Mathlib.RingTheory.HopfAlgebra.Quotient
 public import Mathlib.RingTheory.HopfAlgebra.TensorProduct
 public import Mathlib.RingTheory.HopkinsLevitzki
diff --git a/Mathlib/RingTheory/Bialgebra/Primitive.lean b/Mathlib/RingTheory/Bialgebra/Primitive.lean
new file mode 100644
index 00000000000000..d292d55f8c6f54
--- /dev/null
+++ b/Mathlib/RingTheory/Bialgebra/Primitive.lean
@@ -0,0 +1,109 @@
+/-
+Copyright (c) 2026 Robert Hawkins. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Robert Hawkins
+-/
+module
+
+public import Mathlib.RingTheory.Bialgebra.Equiv
+
+/-!
+# Primitive elements in a bialgebra
+
+This file defines primitive elements in a bialgebra, i.e. elements `a` such that
+`Δ a = a ⊗ₜ 1 + 1 ⊗ₜ a` and `ε a = 0`.
+
+## Main declarations
+
+* `IsPrimitiveElem R a`: `a` is a primitive element of the `R`-bialgebra.
+* `primitiveSubmodule R A`: The submodule of primitive elements of `A`.
+
+## TODO
+
+* `primitiveSubmodule` is a `LieSubalgebra` with bracket `[a, b] = a * b - b * a`.
+  (`IsPrimitiveElem.commutator` is stated with `a * b - b * a` rather than `⁅a, b⁆` to avoid
+  importing Lie theory into this file.)
+* (Milnor–Moore) In characteristic 0 over a field, the primitive elements of a
+  cocommutative connected bialgebra generate it as the universal enveloping of a Lie algebra.
+* Generalize to `(g, h)`-skew-primitive elements `Δ a = a ⊗ₜ g + h ⊗ₜ a` for group-like `g`, `h`
+  over a plain coalgebra, of which primitivity is the `(1, 1)` case over a bialgebra.
+-/
+
+public section
+
+open Coalgebra TensorProduct
+
+variable {F R A B : Type*}
+
+section Semiring
+variable [CommSemiring R] [Semiring A] [Bialgebra R A] [Semiring B] [Bialgebra R B] {a b : A}
+
+variable (R) in
+/-- An element `a` of a bialgebra is *primitive* if `Δ a = a ⊗ₜ 1 + 1 ⊗ₜ a` and `ε a = 0`,
+where `ε` and `Δ` are the counit and comultiplication respectively. -/
+@[mk_iff]
+structure IsPrimitiveElem (a : A) : Prop where
+  /-- A primitive element `a` satisfies `ε(a) = 0`. -/
+  counit_eq_zero : counit (R := R) a = 0
+  /-- A primitive element `a` satisfies `Δ(a) = a ⊗ₜ 1 + 1 ⊗ₜ a`. -/
+  comul_eq_tmul_add_tmul : comul a = a ⊗ₜ[R] 1 + 1 ⊗ₜ[R] a
+
+attribute [simp] IsPrimitiveElem.counit_eq_zero IsPrimitiveElem.comul_eq_tmul_add_tmul
+
+/-- In a bialgebra, `0` is a primitive element. -/
+lemma IsPrimitiveElem.zero : IsPrimitiveElem R (0 : A) := by simp [isPrimitiveElem_iff]
+
+/-- In a bialgebra over a nontrivial semiring, primitive elements are not `1`. -/
+lemma IsPrimitiveElem.ne_one [Nontrivial R] (ha : IsPrimitiveElem R a) : a ≠ 1 :=
+  ne_of_apply_ne (counit (R := R)) (by simp [ha])
+
+/-- Primitive elements in a bialgebra are stable under addition. -/
+lemma IsPrimitiveElem.add (ha : IsPrimitiveElem R a) (hb : IsPrimitiveElem R b) :
+    IsPrimitiveElem R (a + b) := ⟨by simp [ha, hb], by simp [ha, hb, add_tmul, tmul_add]; abel⟩
+
+/-- Primitive elements in a bialgebra are stable under scalar multiplication. -/
+lemma IsPrimitiveElem.smul (ha : IsPrimitiveElem R a) (r : R) : IsPrimitiveElem R (r • a) :=
+  ⟨by simp [ha], by simp [ha, smul_add, smul_tmul']⟩
+
+/-- A bialgebra homomorphism sends primitive elements to primitive elements. -/
+lemma IsPrimitiveElem.map [FunLike F A B] [BialgHomClass F R A B] (f : F)
+    (ha : IsPrimitiveElem R a) : IsPrimitiveElem R (f a) :=
+  ⟨by simp [ha], by simp [ha, ← CoalgHomClass.map_comp_comul_apply]⟩
+
+/-- A bialgebra isomorphism preserves primitive elements. -/
+@[simp] lemma isPrimitiveElem_map_equiv [EquivLike F A B] [BialgEquivClass F R A B] (f : F) :
+    IsPrimitiveElem R (f a) ↔ IsPrimitiveElem R a where
+  mp ha := (BialgEquivClass.toBialgEquiv f).symm_apply_apply a ▸ ha.map _
+  mpr := .map f
+
+variable (R A) in
+/-- The primitive elements form a submodule. -/
+def primitiveSubmodule : Submodule R A where
+  carrier := {a | IsPrimitiveElem R a}
+  add_mem' := .add
+  zero_mem' := .zero
+  smul_mem' r _ ha := ha.smul r
+
+@[simp] lemma mem_primitiveSubmodule : a ∈ primitiveSubmodule R A ↔ IsPrimitiveElem R a := Iff.rfl
+
+end Semiring
+
+section Ring
+variable [CommSemiring R] [Ring A] [Bialgebra R A] {a b : A}
+
+/-- Primitive elements in a bialgebra are stable under negation. -/
+lemma IsPrimitiveElem.neg (ha : IsPrimitiveElem R a) : IsPrimitiveElem R (-a) :=
+  ⟨by simpa [ha] using (map_add (counit (R := R)) (-a) a).symm,
+    by simp [ha, neg_tmul, tmul_neg, add_comm]⟩
+
+/-- Primitive elements in a bialgebra are stable under subtraction. -/
+lemma IsPrimitiveElem.sub (ha : IsPrimitiveElem R a) (hb : IsPrimitiveElem R b) :
+    IsPrimitiveElem R (a - b) := sub_eq_add_neg a b ▸ ha.add hb.neg
+
+/-- The commutator `[a, b] = a * b - b * a` of two primitive elements is primitive. -/
+lemma IsPrimitiveElem.commutator (ha : IsPrimitiveElem R a) (hb : IsPrimitiveElem R b) :
+    IsPrimitiveElem R (a * b - b * a) :=
+  ⟨by simpa [ha] using (map_add (counit (R := R)) (a * b - b * a) (b * a)).symm,
+    by simp [ha, hb, add_mul, mul_add, sub_tmul, tmul_sub]; abel⟩
+
+end Ring
diff --git a/Mathlib/RingTheory/HopfAlgebra/Generators.lean b/Mathlib/RingTheory/HopfAlgebra/Generators.lean
new file mode 100644
index 00000000000000..9eefb28178c03b
--- /dev/null
+++ b/Mathlib/RingTheory/HopfAlgebra/Generators.lean
@@ -0,0 +1,155 @@
+/-
+Copyright (c) 2026 Robert Hawkins. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Robert Hawkins
+-/
+module
+
+public import Mathlib.RingTheory.HopfAlgebra.Convolution
+
+/-!
+# Constructing Hopf algebras from algebra generators
+
+This file provides an extension principle to upgrade a bialgebra to a Hopf algebra given
+antimultiplicative antipode data on generators.
+
+## Main definitions
+
+* `HopfAlgebra.ofGenerators`: construct a Hopf algebra from data on a generating set.
+
+## Main results
+
+* `LinearMap.convMul_eq_one_of_adjoin_eq_top_left` and
+  `LinearMap.convMul_eq_one_of_adjoin_eq_top_right`: a pointwise one-sided convolution inverse of
+  a multiplicative map on generators is a global one.
+* `HopfAlgebra.eq_antipode_of_adjoin_eq_top_left` and
+  `HopfAlgebra.eq_antipode_of_adjoin_eq_top_right`: a one-sided convolution inverse of `id` on a
+  generating set is the antipode.
+-/
+
+public section
+
+open Algebra Coalgebra LinearMap WithConv
+
+variable {R A B : Type*} [CommSemiring R]
+
+namespace LinearMap
+
+section ExtensionPrinciple
+
+/-! ### Extension principle from algebra generators -/
+
+variable [Semiring A] [Bialgebra R A] [Semiring B] [Algebra R B]
+  {g f : A →ₗ[R] B} {s : Set A}
+
+/-- If a unital antimultiplicative map `g` is a left convolution inverse of a unital
+multiplicative map `f` pointwise on an algebra-generating set, then `toConv g * toConv f = 1`. -/
+theorem convMul_eq_one_of_adjoin_eq_top_left
+    (g_one : g 1 = 1) (g_mul : ∀ x y, g (x * y) = g y * g x)
+    (f_one : f 1 = 1) (f_mul : ∀ x y, f (x * y) = f x * f y)
+    (adjoin_eq_top : adjoin R s = ⊤)
+    (g_convMul_f : ∀ p ∈ s, (toConv g * toConv f) p = (1 : WithConv (A →ₗ[R] B)) p) :
+    toConv g * toConv f = 1 := by
+  ext x; refine adjoin_le
+    (S := (eqLocus (toConv g * toConv f).ofConv (ofConv 1)).toSubalgebra ?_ fun a b ha hb ↦ ?_)
+    g_convMul_f (adjoin_eq_top.ge mem_top)
+  · simp [g_one, f_one, TensorProduct.one_def]
+  let 𝓡a := ℛ R a; let 𝓡b := ℛ R b
+  simp only [mem_eqLocus, 𝓡a.convMul_apply, 𝓡b.convMul_apply, convOne_apply] at ha hb ⊢
+  calc (toConv g * toConv f) (a * b)
+      _ = ∑ p ∈ 𝓡a.index, ∑ q ∈ 𝓡b.index,
+            g (𝓡b.left q) * (g (𝓡a.left p) * f (𝓡a.right p)) * f (𝓡b.right q) := by
+        simp [← 𝓡a.eq, ← 𝓡b.eq, Finset.sum_mul_sum, g_mul, f_mul, mul_assoc]
+      _ = algebraMap R B (counit (a * b)) := by
+        rw [Finset.sum_comm]; simp_rw [← Finset.sum_mul, ← Finset.mul_sum, ha, ← commutes]
+        simp_rw [mul_assoc, ← Finset.mul_sum, hb, ← map_mul, ← Bialgebra.counit_mul]
+
+/-- If a unital antimultiplicative map `g` is a right convolution inverse of a unital
+multiplicative map `f` pointwise on an algebra-generating set, then `toConv f * toConv g = 1`. -/
+theorem convMul_eq_one_of_adjoin_eq_top_right
+    (g_one : g 1 = 1) (g_mul : ∀ x y, g (x * y) = g y * g x)
+    (f_one : f 1 = 1) (f_mul : ∀ x y, f (x * y) = f x * f y)
+    (adjoin_eq_top : adjoin R s = ⊤)
+    (f_convMul_g : ∀ p ∈ s, (toConv f * toConv g) p = (1 : WithConv (A →ₗ[R] B)) p) :
+    toConv f * toConv g = 1 := by
+  ext x; refine adjoin_le
+    (S := (eqLocus (toConv f * toConv g).ofConv (ofConv 1)).toSubalgebra ?_ fun a b ha hb ↦ ?_)
+    f_convMul_g (adjoin_eq_top.ge mem_top)
+  · simp [g_one, f_one, TensorProduct.one_def]
+  let 𝓡a := ℛ R a; let 𝓡b := ℛ R b
+  simp only [mem_eqLocus, 𝓡a.convMul_apply, 𝓡b.convMul_apply, convOne_apply] at ha hb ⊢
+  calc (toConv f * toConv g) (a * b)
+      _ = ∑ p ∈ 𝓡a.index, ∑ q ∈ 𝓡b.index,
+            f (𝓡a.left p) * (f (𝓡b.left q) * g (𝓡b.right q)) * g (𝓡a.right p) := by
+        simp [← 𝓡a.eq, ← 𝓡b.eq, Finset.sum_mul_sum, g_mul, f_mul, mul_assoc]
+      _ = algebraMap R B (counit (a * b)) := by
+        simp_rw [← Finset.sum_mul, ← Finset.mul_sum, hb, ← commutes]
+        simp_rw [mul_assoc, ← Finset.mul_sum, ha, ← map_mul, mul_comm (counit b),
+          ← Bialgebra.counit_mul]
+
+end ExtensionPrinciple
+
+end LinearMap
+
+namespace HopfAlgebra
+
+section Construction
+variable [Semiring A] [Bialgebra R A] {S₀ : A →ₗ[R] A} {s : Set A}
+
+variable (S₀) in
+/-- Upgrade a bialgebra to a Hopf algebra from a unital antimultiplicative candidate antipode
+that is a two-sided convolution inverse of the identity pointwise on an algebra-generating
+set. -/
+noncomputable abbrev ofGenerators (S₀_one : S₀ 1 = 1) (S₀_mul : ∀ x y, S₀ (x * y) = S₀ y * S₀ x)
+    (adjoin_eq_top : adjoin R s = ⊤)
+    (S₀_convMul_id : ∀ p ∈ s,
+      (toConv S₀ * toConv (.id : A →ₗ[R] A)) p = (1 : WithConv (A →ₗ[R] A)) p)
+    (id_convMul_S₀ : ∀ p ∈ s,
+      (toConv (.id : A →ₗ[R] A) * toConv S₀) p = (1 : WithConv (A →ₗ[R] A)) p) :
+    HopfAlgebra R A :=
+  ofConvInverse S₀
+    (convMul_eq_one_of_adjoin_eq_top_left S₀_one S₀_mul rfl (fun _ _ ↦ rfl)
+      adjoin_eq_top S₀_convMul_id)
+    (convMul_eq_one_of_adjoin_eq_top_right S₀_one S₀_mul rfl (fun _ _ ↦ rfl)
+      adjoin_eq_top id_convMul_S₀)
+
+end Construction
+
+section Uniqueness
+variable [Semiring A] [HopfAlgebra R A] {S₀ : A →ₗ[R] A} {s : Set A}
+
+/-- A left convolution inverse of the identity is the antipode. -/
+theorem eq_antipode_of_convMul_id_eq_one (h : toConv S₀ * toConv LinearMap.id = 1) :
+    S₀ = antipode R :=
+  toConv_injective (left_inv_eq_right_inv h id_mul_antipode)
+
+/-- A right convolution inverse of the identity is the antipode. -/
+theorem eq_antipode_of_id_convMul_eq_one (h : toConv LinearMap.id * toConv S₀ = 1) :
+    S₀ = antipode R :=
+  toConv_injective (left_inv_eq_right_inv antipode_mul_id h).symm
+
+/-- A unital antimultiplicative map that is a left convolution inverse of the identity on an
+algebra-generating set is the antipode. -/
+theorem eq_antipode_of_adjoin_eq_top_left (S₀_one : S₀ 1 = 1)
+    (S₀_mul : ∀ x y, S₀ (x * y) = S₀ y * S₀ x) (adjoin_eq_top : adjoin R s = ⊤)
+    (S₀_convMul_id : ∀ p ∈ s,
+      (toConv S₀ * toConv (.id : A →ₗ[R] A)) p = (1 : WithConv (A →ₗ[R] A)) p) :
+    S₀ = antipode R :=
+  eq_antipode_of_convMul_id_eq_one
+    (convMul_eq_one_of_adjoin_eq_top_left S₀_one S₀_mul rfl (fun _ _ ↦ rfl)
+      adjoin_eq_top S₀_convMul_id)
+
+/-- A unital antimultiplicative map that is a right convolution inverse of the identity on an
+algebra-generating set is the antipode. -/
+theorem eq_antipode_of_adjoin_eq_top_right (S₀_one : S₀ 1 = 1)
+    (S₀_mul : ∀ x y, S₀ (x * y) = S₀ y * S₀ x) (adjoin_eq_top : adjoin R s = ⊤)
+    (id_convMul_S₀ : ∀ p ∈ s,
+      (toConv (.id : A →ₗ[R] A) * toConv S₀) p = (1 : WithConv (A →ₗ[R] A)) p) :
+    S₀ = antipode R :=
+  eq_antipode_of_id_convMul_eq_one
+    (convMul_eq_one_of_adjoin_eq_top_right S₀_one S₀_mul rfl (fun _ _ ↦ rfl)
+      adjoin_eq_top id_convMul_S₀)
+
+end Uniqueness
+
+end HopfAlgebra
diff --git a/Mathlib/RingTheory/HopfAlgebra/Primitive.lean b/Mathlib/RingTheory/HopfAlgebra/Primitive.lean
new file mode 100644
index 00000000000000..8d62d446eb88d6
--- /dev/null
+++ b/Mathlib/RingTheory/HopfAlgebra/Primitive.lean
@@ -0,0 +1,75 @@
+/-
+Copyright (c) 2026 Robert Hawkins. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Robert Hawkins
+-/
+module
+
+public import Mathlib.RingTheory.Bialgebra.Primitive
+public import Mathlib.RingTheory.HopfAlgebra.Generators
+
+/-!
+# Primitive elements in a Hopf algebra
+
+Facts about primitive elements in a Hopf algebra, plus `HopfAlgebra.ofPrimitives`,
+a constructor for Hopf algebras generated as algebras by primitive elements.
+
+## Main declarations
+
+* `IsPrimitiveElem.antipode_eq_neg`: the antipode sends primitive elements to their negation.
+* `IsPrimitiveElem.antipode`: the antipode preserves primitivity.
+* `HopfAlgebra.ofPrimitives`: construct a Hopf algebra from a primitive-element generating set.
+* `HopfAlgebra.eq_antipodeAlgHomOp_of_primitives`: the antipode is the unique anti-algebra hom
+  negating a primitive generating set.
+-/
+
+public section
+
+open HopfAlgebra LinearMap MulOpposite
+
+variable {R A : Type*} [CommSemiring R] [Ring A]
+
+section
+variable [HopfAlgebra R A] {a : A}
+
+/-- The antipode of a Hopf algebra sends primitive elements to their negation. -/
+@[simp] theorem IsPrimitiveElem.antipode_eq_neg (ha : IsPrimitiveElem R a) : antipode R a = -a := by
+  simpa [ha, eq_neg_iff_add_eq_zero] using mul_antipode_rTensor_comul_apply (R := R) a
+
+/-- The antipode preserves primitivity. -/
+protected lemma IsPrimitiveElem.antipode (ha : IsPrimitiveElem R a) :
+    IsPrimitiveElem R (antipode R a) := ha.antipode_eq_neg ▸ ha.neg
+
+/-- The antipode is involutive on primitive elements. -/
+lemma IsPrimitiveElem.antipode_antipode (ha : IsPrimitiveElem R a) :
+    antipode R (antipode R a) = a := by simp [ha.antipode_eq_neg, ha.neg.antipode_eq_neg]
+
+end
+
+namespace HopfAlgebra
+
+/-- Upgrade a bialgebra generated by primitive elements to a Hopf algebra by specifying the
+antipode-on-generators formula `S p = op (-p)`. -/
+noncomputable abbrev ofPrimitives [Bialgebra R A] (S : A →ₐ[R] Aᵐᵒᵖ) {s : Set A}
+    (adjoin_eq_top : Algebra.adjoin R s = ⊤)
+    (prim : ∀ p ∈ s, IsPrimitiveElem R p)
+    (S_apply : ∀ p ∈ s, S p = op (-p)) :
+    HopfAlgebra R A :=
+  ofGenerators ((opLinearEquiv R).symm.toLinearMap ∘ₗ S.toLinearMap)
+    (by simp) (fun _ _ ↦ by simp) adjoin_eq_top
+    (fun p hp ↦ by simp [convMul_apply, prim p hp, S_apply p hp])
+    (fun p hp ↦ by simp [convMul_apply, prim p hp, S_apply p hp])
+
+/-- On a Hopf algebra generated by primitive elements, the antipode is the unique anti-algebra hom
+negating the generators. -/
+theorem eq_antipodeAlgHomOp_of_primitives [HopfAlgebra R A] (S : A →ₐ[R] Aᵐᵒᵖ) {s : Set A}
+    (adjoin_eq_top : Algebra.adjoin R s = ⊤) (prim : ∀ p ∈ s, IsPrimitiveElem R p)
+    (S_apply : ∀ p ∈ s, S p = op (-p)) :
+    S = antipodeAlgHomOp R A := by
+  have h := eq_antipode_of_adjoin_eq_top_left (S₀ := (opLinearEquiv R).symm.toLinearMap ∘ₗ
+    S.toLinearMap) (by simp) (fun _ _ ↦ by simp) adjoin_eq_top
+    (fun p hp ↦ by simp [convMul_apply, prim p hp, S_apply p hp])
+  ext a
+  simpa using congr(op ($h a))
+
+end HopfAlgebra