refactor(*): replace comm_ring/integral_domain with ring/domain where…

… possible (#9739)




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

src/algebra/algebra/subalgebra.lean

@@ -372,6 +372,10 @@ 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

src/data/polynomial/derivative.lean

@@ -303,7 +303,7 @@ end
 end comm_ring
 
 section domain
-variables [comm_ring R] [integral_domain R]
+variables [ring R] [domain R]
 
 lemma mem_support_derivative [char_zero R] (p : polynomial R) (n : ℕ) :
   n ∈ (derivative p).support ↔ n + 1 ∈ p.support :=

src/data/polynomial/integral_normalization.lean

@@ -74,7 +74,7 @@ monic_of_degree_le f.nat_degree
 end semiring
 
 section domain
-variables [comm_ring R] [integral_domain R]
+variables [ring R] [domain R]
 
 @[simp] lemma support_integral_normalization {f : polynomial R} :
   (integral_normalization f).support = f.support :=
@@ -86,7 +86,10 @@ begin
   intro hfi,
   split_ifs with hi; simp [hfi, hi, pow_ne_zero _ (leading_coeff_ne_zero.mpr hf)]
 end
+end domain
 
+section integral_domain
+variables [comm_ring R] [integral_domain R]
 variables [comm_ring S]
 
 lemma integral_normalization_eval₂_eq_zero {p : polynomial R} (f : R →+* S)
@@ -127,7 +130,7 @@ lemma integral_normalization_aeval_eq_zero [algebra R S] {f : polynomial R}
   aeval (z * algebra_map R S f.leading_coeff) (integral_normalization f) = 0 :=
 integral_normalization_eval₂_eq_zero (algebra_map R S) hz inj
 
-end domain
+end integral_domain
 
 end integral_normalization
 

src/data/polynomial/mirror.lean

@@ -131,18 +131,20 @@ by rw [leading_coeff, trailing_coeff, mirror_nat_trailing_degree, coeff_mirror,
 lemma mirror_leading_coeff : p.mirror.leading_coeff = p.trailing_coeff :=
 by rw [←p.mirror_mirror, mirror_trailing_coeff, p.mirror_mirror]
 
-lemma mirror_mul_of_domain {R : Type*} [comm_ring R] [integral_domain R] (p q : polynomial R) :
+lemma mirror_mul_of_domain {R : Type*} [ring R] [domain R] (p q : polynomial R) :
   (p * q).mirror = p.mirror * q.mirror :=
 begin
   by_cases hp : p = 0,
   { rw [hp, zero_mul, mirror_zero, zero_mul] },
   by_cases hq : q = 0,
   { rw [hq, mul_zero, mirror_zero, mul_zero] },
   rw [mirror, mirror, mirror, reverse_mul_of_domain, nat_trailing_degree_mul hp hq, pow_add],
-  ring,
+  rw [mul_assoc, ←mul_assoc q.reverse],
+  conv_lhs { congr, skip, congr, rw [←X_pow_mul] },
+  repeat { rw [mul_assoc], },
 end
 
-lemma mirror_smul {R : Type*} [comm_ring R] [integral_domain R] (p : polynomial R) (a : R) :
+lemma mirror_smul {R : Type*} [ring R] [domain R] (p : polynomial R) (a : R) :
   (a • p).mirror = a • p.mirror :=
 by rw [←C_mul', ←C_mul', mirror_mul_of_domain, mirror_C]
 

src/data/polynomial/reverse.lean

@@ -253,7 +253,7 @@ begin
   simp [reverse_mul, *],
 end
 
-lemma trailing_coeff_mul {R : Type*} [comm_ring R] [integral_domain R] (p q : polynomial R) :
+lemma trailing_coeff_mul {R : Type*} [ring R] [domain R] (p q : polynomial R) :
   (p * q).trailing_coeff = p.trailing_coeff * q.trailing_coeff :=
 by rw [←reverse_leading_coeff, reverse_mul_of_domain, leading_coeff_mul,
   reverse_leading_coeff, reverse_leading_coeff]

src/data/polynomial/ring_division.lean

@@ -80,7 +80,7 @@ def mod_by_monic_hom [nontrivial R] (hq : q.monic) :
 end comm_ring
 
 section no_zero_divisors
-variables [comm_ring R] [no_zero_divisors R] {p q : polynomial R}
+variables [ring R] [no_zero_divisors R] {p q : polynomial R}
 
 instance : no_zero_divisors (polynomial R) :=
 { eq_zero_or_eq_zero_of_mul_eq_zero := λ a b h, begin
@@ -103,12 +103,6 @@ then if hn0 : n = 0 then by simp [hp0, hn0]
 else nat_degree_pow'
   (by rw [← leading_coeff_pow, ne.def, leading_coeff_eq_zero]; exact pow_ne_zero _ hp0)
 
-lemma root_mul : is_root (p * q) a ↔ is_root p a ∨ is_root q a :=
-by simp_rw [is_root, eval_mul, mul_eq_zero]
-
-lemma root_or_root_of_root_mul (h : is_root (p * q) a) : is_root p a ∨ is_root q a :=
-root_mul.1 h
-
 lemma degree_le_mul_left (p : polynomial R) (hq : q ≠ 0) : degree p ≤ degree (p * q) :=
 if hp : p = 0 then by simp only [hp, zero_mul, le_refl]
 else by rw [degree_mul, degree_eq_nat_degree hp,
@@ -124,13 +118,24 @@ end
 
 end no_zero_divisors
 
-section integral_domain
-variables [comm_ring R] [integral_domain R] {p q : polynomial R}
+section no_zero_divisors
+variables [comm_ring R] [no_zero_divisors R] {p q : polynomial R}
 
-instance : integral_domain (polynomial R) :=
+lemma root_mul : is_root (p * q) a ↔ is_root p a ∨ is_root q a :=
+by simp_rw [is_root, eval_mul, mul_eq_zero]
+
+lemma root_or_root_of_root_mul (h : is_root (p * q) a) : is_root p a ∨ is_root q a :=
+root_mul.1 h
+
+end no_zero_divisors
+
+section domain
+variables [ring R] [domain R] {p q : polynomial R}
+
+instance : domain (polynomial R) :=
 { ..polynomial.no_zero_divisors,
   ..polynomial.nontrivial,
-  ..polynomial.comm_ring }
+  ..polynomial.ring }
 
 lemma nat_trailing_degree_mul (hp : p ≠ 0) (hq : q ≠ 0) :
   (p * q).nat_trailing_degree = p.nat_trailing_degree + q.nat_trailing_degree :=
@@ -141,6 +146,16 @@ begin
     nat.add_sub_assoc (nat.sub_le _ _), add_comm, nat.add_sub_assoc (nat.sub_le _ _)],
 end
 
+end domain
+
+section integral_domain
+variables [comm_ring R] [integral_domain R] {p q : polynomial R}
+
+instance : integral_domain (polynomial R) :=
+{ ..polynomial.no_zero_divisors,
+  ..polynomial.nontrivial,
+  ..polynomial.comm_ring }
+
 section roots
 
 open multiset

src/data/real/cau_seq.lean

@@ -402,8 +402,8 @@ by rw mul_comm; apply mul_equiv_zero _ hf
 
 end comm_ring
 
-section integral_domain
-variables {β : Type*} [comm_ring β] [integral_domain β] (abv : β → α) [is_absolute_value abv]
+section domain
+variables {β : Type*} [ring β] [domain β] (abv : β → α) [is_absolute_value abv]
 
 lemma one_not_equiv_zero : ¬ (const abv 1) ≈ (const abv 0) :=
 assume h,
@@ -417,7 +417,7 @@ have abv 1 = 0, from le_antisymm h1 h2,
 have (1 : β) = 0, from (is_absolute_value.abv_eq_zero abv).1 this,
 absurd this one_ne_zero
 
-end integral_domain
+end domain
 
 section field
 variables {β : Type*} [field β] {abv : β → α} [is_absolute_value abv]

src/field_theory/fixed.lean

@@ -265,7 +265,7 @@ end
 end fixed_points
 
 lemma linear_independent_to_linear_map (R : Type u) (A : Type v) (B : Type w)
-  [comm_semiring R] [comm_ring A] [algebra R A]
+  [comm_semiring R] [ring A] [algebra R A]
   [comm_ring B] [integral_domain B] [algebra R B] :
   linear_independent B (alg_hom.to_linear_map : (A →ₐ[R] B) → (A →ₗ[R] B)) :=
 have linear_independent B (linear_map.lto_fun R A B ∘ alg_hom.to_linear_map),

src/linear_algebra/finite_dimensional.lean

@@ -1047,18 +1047,25 @@ noncomputable def alg_equiv_equiv_alg_hom (F : Type u) [field F] (E : Type v) [f
 
 section
 
-/-- An integral domain that is module-finite as an algebra over a field is a field. -/
-noncomputable def field_of_finite_dimensional
-  (F K : Type*) [field F] [comm_ring K] [integral_domain K]
-  [algebra F K] [finite_dimensional F K] : field K :=
+/-- An domain that is module-finite as an algebra over a field is a division ring. -/
+noncomputable def division_ring_of_finite_dimensional
+  (F K : Type*) [field F] [ring K] [domain K]
+  [algebra F K] [finite_dimensional F K] : division_ring K :=
 { inv := λ x, if H : x = 0 then 0 else classical.some $
     (show function.surjective (algebra.lmul_left F x), from
       linear_map.injective_iff_surjective.1 $ λ _ _, (mul_right_inj' H).1) 1,
   mul_inv_cancel := λ x hx, show x * dite _ _ _ = _, by { rw dif_neg hx,
     exact classical.some_spec ((show function.surjective (algebra.lmul_left F x), from
       linear_map.injective_iff_surjective.1 $ λ _ _, (mul_right_inj' hx).1) 1) },
   inv_zero := dif_pos rfl,
-  .. ‹integral_domain K›,
+  .. ‹domain K›,
+  .. ‹ring K› }
+
+/-- An integral domain that is module-finite as an algebra over a field is a field. -/
+noncomputable def field_of_finite_dimensional
+  (F K : Type*) [field F] [comm_ring K] [integral_domain K]
+  [algebra F K] [finite_dimensional F K] : field K :=
+{ .. division_ring_of_finite_dimensional F K,
   .. ‹comm_ring K› }
 
 end

src/linear_algebra/free_module/pid.lean

@@ -48,11 +48,11 @@ free module, finitely generated module, rank, structure theorem
 
 open_locale big_operators
 
-section comm_ring
-
 universes u v
 
-variables {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M]
+section ring
+
+variables {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M]
 variables {ι : Type*} (b : basis ι R M)
 
 open submodule.is_principal
@@ -136,6 +136,15 @@ begin
   exact (linear_map.mem_submodule_image_of_le hNO).mpr ⟨x, hx, rfl⟩
 end
 
+end ring
+
+section comm_ring
+
+variables {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M]
+variables {ι : Type*} (b : basis ι R M)
+
+open submodule.is_principal
+
 -- Note that the converse may not hold if `ϕ` is not injective.
 lemma generator_map_dvd_of_mem {N : submodule R M}
   (ϕ : M →ₗ[R] R) [(N.map ϕ).is_principal] {x : M} (hx : x ∈ N) :
@@ -150,9 +159,9 @@ by { rw [← mem_iff_generator_dvd, linear_map.mem_submodule_image_of_le hNO], e
 
 end comm_ring
 
-section integral_domain
+section domain
 
-variables {ι : Type*} {R : Type*} [comm_ring R] [integral_domain R]
+variables {ι : Type*} {R : Type*} [ring R] [domain R]
 variables {M : Type*} [add_comm_group M] [module R M] {b : ι → M}
 
 lemma not_mem_of_ortho {x : M} {N : submodule R M}
@@ -308,6 +317,13 @@ lemma basis.card_le_card_of_le
 b.card_le_card_of_linear_independent
   (b'.linear_independent.map' (submodule.of_le hNO) (N.ker_of_le O _))
 
+end domain
+
+section integral_domain
+
+variables {ι : Type*} {R : Type*} [comm_ring R] [integral_domain R]
+variables {M : Type*} [add_comm_group M] [module R M] {b : ι → M}
+
 /-- If `N` is a submodule in a free, finitely generated module,
 do induction on adjoining a linear independent element to a submodule. -/
 def submodule.induction_on_rank [fintype ι] (b : basis ι R M) (P : submodule R M → Sort*)

src/linear_algebra/matrix/nonsingular_inverse.lean

@@ -705,7 +705,7 @@ by rw [cramer_eq_adjugate_mul_vec, mul_vec_mul_vec, mul_adjugate, smul_mul_vec_a
 
 section nondegenerate
 
-variables {m R A : Type*} [fintype m] [comm_ring R] [comm_ring A] [integral_domain A]
+variables {m R A : Type*} [fintype m] [comm_ring R]
 
 /-- A matrix `M` is nondegenerate if for all `v ≠ 0`, there is a `w ≠ 0` with `w ⬝ M ⬝ v ≠ 0`. -/
 def nondegenerate (M : matrix m m R) :=
@@ -721,6 +721,8 @@ lemma nondegenerate.exists_not_ortho_of_ne_zero {M : matrix m m R} (hM : nondege
   {v : m → R} (hv : v ≠ 0) : ∃ w, matrix.dot_product v (mul_vec M w) ≠ 0 :=
 not_forall.mp (mt hM.eq_zero_of_ortho hv)
 
+variables [comm_ring A] [integral_domain A]
+
 /-- If `M` has a nonzero determinant, then `M` as a bilinear form on `n → A` is nondegenerate.
 
 See also `bilin_form.nondegenerate_of_det_ne_zero'` and `bilin_form.nondegenerate_of_det_ne_zero`.

src/ring_theory/hahn_series.lean

@@ -738,8 +738,8 @@ instance [comm_ring R] : comm_ring (hahn_series Γ R) :=
 { .. hahn_series.comm_semiring,
   .. hahn_series.ring }
 
-instance {Γ} [linear_ordered_cancel_add_comm_monoid Γ] [comm_ring R] [integral_domain R] :
-  integral_domain (hahn_series Γ R) :=
+instance {Γ} [linear_ordered_cancel_add_comm_monoid Γ] [ring R] [domain R] :
+  domain (hahn_series Γ R) :=
 { eq_zero_or_eq_zero_of_mul_eq_zero := λ x y xy, begin
     by_cases hx : x = 0,
     { left, exact hx },
@@ -751,10 +751,15 @@ instance {Γ} [linear_ordered_cancel_add_comm_monoid Γ] [comm_ring R] [integral
     simp [coeff_order_ne_zero, hx, xy],
   end,
   .. hahn_series.nontrivial,
+  .. hahn_series.ring }
+
+instance {Γ} [linear_ordered_cancel_add_comm_monoid Γ] [comm_ring R] [integral_domain R] :
+  integral_domain (hahn_series Γ R) :=
+{ .. hahn_series.domain,
   .. hahn_series.comm_ring }
 
 @[simp]
-lemma order_mul {Γ} [linear_ordered_cancel_add_comm_monoid Γ] [comm_ring R] [integral_domain R]
+lemma order_mul {Γ} [linear_ordered_cancel_add_comm_monoid Γ] [ring R] [domain R]
   {x y : hahn_series Γ R} (hx : x ≠ 0) (hy : y ≠ 0) :
   (x * y).order = x.order + y.order :=
 begin
@@ -1026,7 +1031,7 @@ end algebra
 
 section valuation
 
-variables [linear_ordered_add_comm_group Γ] [comm_ring R] [integral_domain R]
+variables [linear_ordered_add_comm_group Γ] [ring R] [domain R]
 
 instance : linear_ordered_comm_group (multiplicative Γ) :=
 { .. (infer_instance : linear_order (multiplicative Γ)),
@@ -1087,7 +1092,7 @@ end
 end valuation
 
 lemma is_pwo_Union_support_powers
-  [linear_ordered_add_comm_group Γ] [comm_ring R] [integral_domain R]
+  [linear_ordered_add_comm_group Γ] [ring R] [domain R]
   {x : hahn_series Γ R} (hx : 0 < add_val Γ R x) :
   (⋃ n : ℕ, (x ^ n).support).is_pwo :=
 begin

src/ring_theory/ideal/basic.lean

@@ -152,7 +152,7 @@ end
 theorem zero_ne_one_of_proper {I : ideal α} (h : I ≠ ⊤) : (0:α) ≠ 1 :=
 λ hz, I.ne_top_iff_one.1 h $ hz ▸ I.zero_mem
 
-lemma bot_prime {R : Type*} [comm_ring R] [integral_domain R] : (⊥ : ideal R).is_prime :=
+lemma bot_prime {R : Type*} [ring R] [domain R] : (⊥ : ideal R).is_prime :=
 ⟨λ h, one_ne_zero (by rwa [ideal.eq_top_iff_one, submodule.mem_bot] at h),
  λ x y h, mul_eq_zero.mp (by simpa only [submodule.mem_bot] using h)⟩
 

src/ring_theory/ideal/operations.lean

@@ -1299,8 +1299,8 @@ quotient_ker_equiv_of_right_inverse (classical.some_spec hf.has_right_inverse)
 
 end comm_ring
 
-/-- The kernel of a homomorphism to an integral domain is a prime ideal. -/
-lemma ker_is_prime [ring R] [comm_ring S] [integral_domain S] (f : R →+* S) :
+/-- The kernel of a homomorphism to a domain is a prime ideal. -/
+lemma ker_is_prime [ring R] [ring S] [domain S] (f : R →+* S) :
   (ker f).is_prime :=
 ⟨by { rw [ne.def, ideal.eq_top_iff_one], exact not_one_mem_ker f },
 λ x y, by simpa only [mem_ker, f.map_mul] using @eq_zero_or_eq_zero_of_mul_eq_zero S _ _ _ _ _⟩

src/ring_theory/localization.lean

@@ -1275,7 +1275,7 @@ by rw [aeval_def, is_scalar_tower.algebra_map_eq R S R',
 
 end integer_normalization
 
-variables {R M} (S) {A K : Type*} [comm_ring A] [integral_domain A]
+variables {R M} (S) {K : Type*}
 
 lemma to_map_eq_zero_iff {x : R} (hM : M ≤ non_zero_divisors R) :
   algebra_map R S x = 0 ↔ x = 0 :=
@@ -1348,6 +1348,8 @@ begin
     rw [hx, ideal.submodule_span_eq, coe_submodule_span_singleton] }
 end
 
+variables {A : Type*} [comm_ring A] [integral_domain A]
+
 /-- A `comm_ring` `S` which is the localization of an integral domain `R` at a subset of
 non-zero elements is an integral domain.
 See note [reducible non-instances]. -/