docs(Algebra/Order/Ring/Defs): tiny IsDomain corrections (#8489)

Co-authored-by: Yaël Dillies <[email protected]>
leanprover-community · Dec 12, 2023 · 8e572f2 · 8e572f2
1 parent 669cc3a
commit 8e572f2
Showing 1 changed file with 2 additions and 3 deletions.
diff --git a/Mathlib/Algebra/Order/Ring/Defs.lean b/Mathlib/Algebra/Order/Ring/Defs.lean
@@ -100,13 +100,12 @@ immediate predecessors and what conditions are added to each of them.
   - `StrictOrderedRing` & totality of the order
   - `LinearOrderedSemiring` & additive inverses
   - `LinearOrderedAddCommGroup` & multiplication & `*` respects `<`
-  - `Domain` & linear order structure
+  - `Ring` & `IsDomain` & linear order structure
 * `LinearOrderedCommRing`
   - `StrictOrderedCommRing` & totality of the order
   - `LinearOrderedRing` & commutativity of multiplication
   - `LinearOrderedCommSemiring` & additive inverses
-  - `IsDomain` & linear order structure
-
+  - `CommRing` & `IsDomain` & linear order structure
 -/
 
 open Function