style(RingTheory/HopfAlgebra/Primitive): file-level Ring binder

Author: hawkrobe

Mathlib/RingTheory/HopfAlgebra/Primitive.lean

@@ -27,10 +27,10 @@ public section
 
 open HopfAlgebra LinearMap MulOpposite
 
-variable {R A : Type*} [CommSemiring R]
+variable {R A : Type*} [CommSemiring R] [Ring A]
 
-section Ring
-variable [Ring A] [HopfAlgebra R A] {a : 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
@@ -44,12 +44,10 @@ protected lemma IsPrimitiveElem.antipode (ha : IsPrimitiveElem R a) :
 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 Ring
+end
 
 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 [Bialgebra R A] (S : A →ₐ[R] Aᵐᵒᵖ) {s : Set A}