trim structure reference from counit lemma docstring

Author: hawkrobe

Mathlib/RingTheory/Coalgebra/Primitive.lean

@@ -97,8 +97,8 @@ def skewPrimitive : Submodule R A where
 
 variable [IsCancelAdd A]
 
-/-- When `g` and `h` have counit `1` (e.g. when they are group-like), the counit condition in
-`IsSkewPrimitiveElem` follows from the comultiplication condition. -/
+/-- When `g` and `h` have counit `1` (e.g. when they are group-like), the counit condition
+follows from the comultiplication condition. -/
 lemma counit_eq_zero_of_comul_eq_tmul_add_tmul (hg : counit (R := R) g = 1)
     (hh : counit (R := R) h = 1) (ha : comul a = g ⊗ₜ[R] a + a ⊗ₜ[R] h) :
     counit (R := R) a = 0 := by