doc(Algebra/Ring): add docstring for CommRing and CommSemiring (#…

…11894)

This PR resolves some nolints by adding docstrings for `CommRing` and `CommSemiring`.

Mathlib/Algebra/Ring/Defs.lean

@@ -260,6 +260,7 @@ multiplication by zero law (`MulZeroClass`). -/
 class NonUnitalCommSemiring (α : Type u) extends NonUnitalSemiring α, CommSemigroup α
 #align non_unital_comm_semiring NonUnitalCommSemiring
 
+/-- A commutative semiring is a semiring with commutative multiplication. -/
 class CommSemiring (R : Type u) extends Semiring R, CommMonoid R
 #align comm_semiring CommSemiring
 
@@ -453,6 +454,7 @@ instance (priority := 100) NonUnitalCommRing.toNonUnitalCommSemiring [s : NonUni
   { s with }
 #align non_unital_comm_ring.to_non_unital_comm_semiring NonUnitalCommRing.toNonUnitalCommSemiring
 
+/-- A commutative ring is a ring with commutative multiplication. -/
 class CommRing (α : Type u) extends Ring α, CommMonoid α
 #align comm_ring CommRing
 
@@ -470,13 +472,13 @@ instance (priority := 100) CommRing.toAddCommGroupWithOne [s : CommRing α] :
     AddCommGroupWithOne α :=
   { s with }
 
-/-- A domain is a nontrivial semiring such multiplication by a non zero element is cancellative,
-  on both sides. In other words, a nontrivial semiring `R` satisfying
-  `∀ {a b c : R}, a ≠ 0 → a * b = a * c → b = c` and
-  `∀ {a b c : R}, b ≠ 0 → a * b = c * b → a = c`.
+/-- A domain is a nontrivial semiring such that multiplication by a non zero element
+is cancellative on both sides. In other words, a nontrivial semiring `R` satisfying
+`∀ {a b c : R}, a ≠ 0 → a * b = a * c → b = c` and
+`∀ {a b c : R}, b ≠ 0 → a * b = c * b → a = c`.
 
-  This is implemented as a mixin for `Semiring α`.
-  To obtain an integral domain use `[CommRing α] [IsDomain α]`. -/
+This is implemented as a mixin for `Semiring α`.
+To obtain an integral domain use `[CommRing α] [IsDomain α]`. -/
 class IsDomain (α : Type u) [Semiring α] extends IsCancelMulZero α, Nontrivial α : Prop
 #align is_domain IsDomain
 

scripts/nolints.json

@@ -3,8 +3,6 @@
  ["docBlame", "AsTrue"],
  ["docBlame", "Associative"],
  ["docBlame", "BinTree"],
- ["docBlame", "CommRing"],
- ["docBlame", "CommSemiring"],
  ["docBlame", "Commutative"],
  ["docBlame", "Computable"],
  ["docBlame", "Computable₂"],