style(RingTheory/HopfAlgebra/Primitive): lift shared Ring binder

Author: hawkrobe

Mathlib/RingTheory/HopfAlgebra/Primitive.lean

@@ -48,9 +48,11 @@ end Ring
 
 namespace HopfAlgebra
 
+variable [Ring A]
+
 /-- 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 [Ring A] [Bialgebra R A] (S : A →ₐ[R] Aᵐᵒᵖ) {s : Set A}
+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)) :
@@ -62,8 +64,8 @@ noncomputable abbrev ofPrimitives [Ring A] [Bialgebra R A] (S : A →ₐ[R] Aᵐ
 
 /-- On a Hopf algebra generated by primitive elements, the antipode is the unique anti-algebra hom
 negating the generators. -/
-theorem eq_antipodeAlgHomOp_of_primitives [Ring A] [HopfAlgebra R A] (S : A →ₐ[R] Aᵐᵒᵖ)
-    {s : Set A} (adjoin_eq_top : Algebra.adjoin R s = ⊤) (prim : ∀ p ∈ s, IsPrimitiveElem R p)
+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 ∘ₗ