From 8e572f2640fb47dc1c0906a1df4af69ea504daa8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Dvo=C5=99=C3=A1k?= Date: Tue, 12 Dec 2023 12:47:15 +0000 Subject: [PATCH] docs(Algebra/Order/Ring/Defs): tiny `IsDomain` corrections (#8489) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Yaël Dillies --- Mathlib/Algebra/Order/Ring/Defs.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Mathlib/Algebra/Order/Ring/Defs.lean b/Mathlib/Algebra/Order/Ring/Defs.lean index 71ce0ad9ca0aa..a2db8c247eec6 100644 --- 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