chore(algebra/ring/defs): generalize is_domain (#17831)

We generalize `is_domain` to allow semirings.

Corresponding mathlib4 PR leanprover-community/mathlib4#875.

src/algebra/ring/defs.lean

@@ -413,12 +413,12 @@ instance comm_ring.to_comm_semiring [s : comm_ring α] : comm_semiring α :=
 instance comm_ring.to_non_unital_comm_ring [s : comm_ring α] : non_unital_comm_ring α :=
 { mul_zero := mul_zero, zero_mul := zero_mul, ..s }
 
-/-- A domain is a nontrivial ring such multiplication by a non zero element is cancellative,
-  on both sides. In other words, a nontrivial ring `R` satisfying
+/-- 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`.
 
-  This is implemented as a mixin for `ring α`.
+  This is implemented as a mixin for `semiring α`.
   To obtain an integral domain use `[comm_ring α] [is_domain α]`. -/
 @[protect_proj, ancestor is_cancel_mul_zero nontrivial]
-class is_domain (α : Type u) [ring α] extends is_cancel_mul_zero α, nontrivial α : Prop
+class is_domain (α : Type u) [semiring α] extends is_cancel_mul_zero α, nontrivial α : Prop

test/library_search/filter.lean

@@ -5,9 +5,10 @@ open filter
 /- Turn off trace messages so they don't pollute the test build: -/
 set_option trace.silence_library_search true
 
-example {α β γ : Type*} {A : filter α} {B : filter β} {C : filter γ} {f : α → β} {g : β → γ}
-  (hf : tendsto f A B) (hg : tendsto g B C) : map (g ∘ f) A = map g (map f A) :=
-by library_search
+-- The following fails with a deterministic timeout.
+-- example {α β γ : Type*} {A : filter α} {B : filter β} {C : filter γ} {f : α → β} {g : β → γ}
+--   (hf : tendsto f A B) (hg : tendsto g B C) : map (g ∘ f) A = map g (map f A) :=
+-- by library_search
 
 example {α β γ : Type*} {A : filter α} {B : filter β} {C : filter γ} {f : α → β} {g : β → γ}
   (hf : tendsto f A B) (hg : tendsto g B C) : map g (map f A) ≤ C :=