refactor(*): remove integral_domain, rename domain to is_domain (#9748)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: kim-em

archive/imo/imo1962_q4.lean

@@ -99,7 +99,7 @@ terms, `a ^ 2 * (2 * a ^ 2 - 1) * (4 * a ^ 2 - 3)`, being equal to zero.
 
 /-- Someday, when there is a Grobner basis tactic, try to automate this proof. (A little tricky --
 the ideals are not the same but their Jacobson radicals are.) -/
-lemma formula {R : Type*} [comm_ring R] [integral_domain R] [char_zero R] (a : R) :
+lemma formula {R : Type*} [comm_ring R] [is_domain R] [char_zero R] (a : R) :
   a ^ 2 + (2 * a ^ 2 - 1) ^ 2 + (4 * a ^ 3 - 3 * a) ^ 2 = 1
   ↔ (2 * a ^ 2 - 1) * (4 * a ^ 3 - 3 * a) = 0 :=
 calc a ^ 2 + (2 * a ^ 2 - 1) ^ 2 + (4 * a ^ 3 - 3 * a) ^ 2 = 1

src/algebra/algebra/basic.lean

@@ -359,7 +359,7 @@ by { convert this, ext, rw [algebra.smul_def, mul_one] },
 smul_left_injective R one_ne_zero
 
 variables {R A}
-lemma iff_algebra_map_injective [ring A] [domain A] [algebra R A] :
+lemma iff_algebra_map_injective [ring A] [is_domain A] [algebra R A] :
   no_zero_smul_divisors R A ↔ function.injective (algebra_map R A) :=
 ⟨@@no_zero_smul_divisors.algebra_map_injective R A _ _ _ _,
  no_zero_smul_divisors.of_algebra_map_injective⟩

src/algebra/algebra/bilinear.lean

@@ -130,17 +130,17 @@ variables {R A : Type*} [comm_semiring R] [ring A] [algebra R A]
 
 lemma lmul_left_injective [no_zero_divisors A] {x : A} (hx : x ≠ 0) :
   function.injective (lmul_left R x) :=
-by { letI : domain A := { exists_pair_ne := ⟨x, 0, hx⟩, ..‹ring A›, ..‹no_zero_divisors A› },
+by { letI : is_domain A := { exists_pair_ne := ⟨x, 0, hx⟩, ..‹ring A›, ..‹no_zero_divisors A› },
      exact mul_right_injective₀ hx }
 
 lemma lmul_right_injective [no_zero_divisors A] {x : A} (hx : x ≠ 0) :
   function.injective (lmul_right R x) :=
-by { letI : domain A := { exists_pair_ne := ⟨x, 0, hx⟩, ..‹ring A›, ..‹no_zero_divisors A› },
+by { letI : is_domain A := { exists_pair_ne := ⟨x, 0, hx⟩, ..‹ring A›, ..‹no_zero_divisors A› },
      exact mul_left_injective₀ hx }
 
 lemma lmul_injective [no_zero_divisors A] {x : A} (hx : x ≠ 0) :
   function.injective (lmul R A x) :=
-by { letI : domain A := { exists_pair_ne := ⟨x, 0, hx⟩, ..‹ring A›, ..‹no_zero_divisors A› },
+by { letI : is_domain A := { exists_pair_ne := ⟨x, 0, hx⟩, ..‹ring A›, ..‹no_zero_divisors A› },
      exact mul_right_injective₀ hx }
 
 end

src/algebra/algebra/subalgebra.lean

@@ -372,13 +372,9 @@ instance no_zero_divisors {R A : Type*} [comm_ring R] [semiring A] [no_zero_divi
   [algebra R A] (S : subalgebra R A) : no_zero_divisors S :=
 S.to_subsemiring.no_zero_divisors
 
-instance domain {R A : Type*} [comm_ring R] [ring A] [domain A] [algebra R A]
-  (S : subalgebra R A) : domain S :=
-subring.domain S.to_subring
-
-instance integral_domain {R A : Type*} [comm_ring R] [comm_ring A] [integral_domain A] [algebra R A]
-  (S : subalgebra R A) : integral_domain S :=
-subring.integral_domain S.to_subring
+instance is_domain {R A : Type*} [comm_ring R] [ring A] [is_domain A] [algebra R A]
+  (S : subalgebra R A) : is_domain S :=
+subring.is_domain S.to_subring
 
 end subalgebra
 

src/algebra/char_p/algebra.lean

@@ -91,7 +91,7 @@ char_p_of_injective_algebra_map (is_fraction_ring.injective R K) p
 lemma char_zero_of_is_fraction_ring [char_zero R] : char_zero K :=
 @char_p.char_p_to_char_zero K _ (char_p_of_is_fraction_ring R 0)
 
-variables [integral_domain R]
+variables [is_domain R]
 
 /-- If `R` has characteristic `p`, then so does `fraction_ring R`. -/
 instance char_p [char_p R p] : char_p (fraction_ring R) p :=

src/algebra/euclidean_domain.lean

@@ -60,9 +60,10 @@ Euclidean domain, transfinite Euclidean domain, Bézout's lemma
 
 universe u
 
-/-- A `euclidean_domain` is an `integral_domain` with a division and a remainder, satisfying
-  `b * (a / b) + a % b = a`. The definition of a euclidean domain usually includes a valuation
-  function `R → ℕ`. This definition is slightly generalised to include a well founded relation
+/-- A `euclidean_domain` is an non-trivial commutative ring with a division and a remainder,
+  satisfying `b * (a / b) + a % b = a`.
+  The definition of a euclidean domain usually includes a valuation function `R → ℕ`.
+  This definition is slightly generalised to include a well founded relation
   `r` with the property that `r (a % b) b`, instead of a valuation.  -/
 @[protect_proj without mul_left_not_lt r_well_founded]
 class euclidean_domain (R : Type u) extends comm_ring R, nontrivial R :=
@@ -317,7 +318,7 @@ by { have := @xgcd_aux_P _ _ _ a b a b 1 0 0 1
 rwa [xgcd_aux_val, xgcd_val] at this }
 
 @[priority 70] -- see Note [lower instance priority]
-instance (R : Type*) [e : euclidean_domain R] : integral_domain R :=
+instance (R : Type*) [e : euclidean_domain R] : is_domain R :=
 by { haveI := classical.dec_eq R, exact
 { eq_zero_or_eq_zero_of_mul_eq_zero :=
     λ a b h, (or_iff_not_and_not.2 $ λ h0,

src/algebra/field.lean

@@ -161,8 +161,8 @@ lemma add_div_eq_mul_add_div (a b : K) {c : K} (hc : c ≠ 0) : a + b / c = (a *
 (eq_div_iff_mul_eq hc).2 $ by rw [right_distrib, (div_mul_cancel _ hc)]
 
 @[priority 100] -- see Note [lower instance priority]
-instance division_ring.to_domain : domain K :=
-{ ..‹division_ring K›, ..(by apply_instance : semiring K),
+instance division_ring.is_domain : is_domain K :=
+{ ..‹division_ring K›,
   ..(by apply_instance : no_zero_divisors K) }
 
 end division_ring
@@ -223,8 +223,8 @@ by rwa [add_comm, add_div', add_comm]
 by simpa using div_sub_div a b hc one_ne_zero
 
 @[priority 100] -- see Note [lower instance priority]
-instance field.to_integral_domain : integral_domain K :=
-{ ..‹field K›, ..division_ring.to_domain }
+instance field.is_domain : is_domain K :=
+{ ..division_ring.is_domain }
 
 end field
 

src/algebra/gcd_monoid/basic.lean

@@ -11,7 +11,7 @@ import data.nat.gcd
 /-!
 # Monoids with normalization functions, `gcd`, and `lcm`
 
-This file defines extra structures on `comm_cancel_monoid_with_zero`s, including `integral_domain`s.
+This file defines extra structures on `comm_cancel_monoid_with_zero`s, including `is_domain`s.
 
 ## Main Definitions
 
@@ -706,9 +706,9 @@ instance normalization_monoid_of_unique_units : normalization_monoid α :=
 
 end unique_unit
 
-section integral_domain
+section is_domain
 
-variables [comm_ring α] [integral_domain α] [normalized_gcd_monoid α]
+variables [comm_ring α] [is_domain α] [normalized_gcd_monoid α]
 
 lemma gcd_eq_of_dvd_sub_right {a b c : α} (h : a ∣ b - c) : gcd a b = gcd a c :=
 begin
@@ -729,7 +729,7 @@ end
 lemma gcd_eq_of_dvd_sub_left {a b c : α} (h : a ∣ b - c) : gcd b a = gcd c a :=
 by rw [gcd_comm _ a, gcd_comm _ a, gcd_eq_of_dvd_sub_right h]
 
-end integral_domain
+end is_domain
 
 section constructors
 noncomputable theory

src/algebra/gcd_monoid/finset.lean

@@ -199,9 +199,9 @@ end gcd
 end finset
 
 namespace finset
-section integral_domain
+section is_domain
 
-variables [comm_ring α] [integral_domain α] [normalized_gcd_monoid α]
+variables [comm_ring α] [is_domain α] [normalized_gcd_monoid α]
 
 lemma gcd_eq_of_dvd_sub {s : finset β} {f g : β → α} {a : α}
   (h : ∀ x : β, x ∈ s → a ∣ f x - g x) :
@@ -218,6 +218,6 @@ begin
   exact congr_arg _ (gcd_eq_of_dvd_sub_right (h _ (mem_insert_self _ _)))
 end
 
-end integral_domain
+end is_domain
 
 end finset

src/algebra/group_power/basic.lean

@@ -416,7 +416,7 @@ by rw [sq, sq, mul_self_sub_mul_self]
 
 alias sq_sub_sq ← pow_two_sub_pow_two
 
-lemma eq_or_eq_neg_of_sq_eq_sq [comm_ring R] [integral_domain R] (a b : R) (h : a ^ 2 = b ^ 2) :
+lemma eq_or_eq_neg_of_sq_eq_sq [comm_ring R] [is_domain R] (a b : R) (h : a ^ 2 = b ^ 2) :
   a = b ∨ a = -b :=
 by rwa [← add_eq_zero_iff_eq_neg, ← sub_eq_zero, or_comm, ← mul_eq_zero,
         ← sq_sub_sq a b, sub_eq_zero]