chore(field_theory/splitting_field): module doc and generalise one le…

…mma (#6739)

This PR provides a module doc for `field_theory.splitting_field`, which is the last file without module doc in `field_theory`. Furthermore, I took the opportunity of renaming the fields in that file from `\alpha`, `\beta`, `\gamma` to `K`, `L`, `F` to make it more readable for newcomers.

Moved `nat_degree_multiset_prod`, to `algebra.polynomial.big_operators`). In order to get the `no_zero_divisors` instance on `polynomial R`, I had to include `data.polynomial.ring_division` in that file. Furthermore, with the help of Damiano, generalised this lemma to `no_zero_divisors R`.

Coauthored by: Damiano Testa adomani@gmail.com



Co-authored-by: Thomas Browning <tb65536@uw.edu>
Co-authored-by: Julian-Kuelshammer <68201724+Julian-Kuelshammer@users.noreply.github.com>

src/algebra/polynomial/big_operators.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson, Jalex Stark
 -/
 import data.polynomial.monic
+import data.polynomial.ring_division
 import tactic.linarith
 /-!
 # Lemmas for the interaction between polynomials and `∑` and `∏`.
@@ -140,7 +141,21 @@ lemma nat_degree_prod [nontrivial R] (h : ∀ i ∈ s, f i ≠ 0) :
 begin
   apply nat_degree_prod',
   rw prod_ne_zero_iff,
-  intros x hx, simp [h x hx],
+  intros x hx, simp [h x hx]
+end
+
+lemma nat_degree_multiset_prod [nontrivial R] (s : multiset (polynomial R))
+  (h : (0 : polynomial R) ∉ s) :
+  nat_degree s.prod = (s.map nat_degree).sum :=
+begin
+  revert h,
+  refine s.induction_on _ _,
+  { simp },
+  intros p s ih h,
+  rw [multiset.mem_cons, not_or_distrib] at h,
+  have hprod : s.prod ≠ 0 := multiset.prod_ne_zero h.2,
+  rw [multiset.prod_cons, nat_degree_mul (ne.symm h.1) hprod, ih h.2,
+    multiset.map_cons, multiset.sum_cons]
 end
 
 /--

src/data/polynomial/ring_division.lean

@@ -47,34 +47,22 @@ eval₂_mod_by_monic_eq_self_of_root hq hx
 
 end comm_ring
 
-section integral_domain
-variables [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) :=
+instance : no_zero_divisors (polynomial R) :=
 { eq_zero_or_eq_zero_of_mul_eq_zero := λ a b h, begin
-    have : leading_coeff 0 = leading_coeff a * leading_coeff b := h ▸ leading_coeff_mul a b,
-    rw [leading_coeff_zero, eq_comm] at this,
-    erw [← leading_coeff_eq_zero, ← leading_coeff_eq_zero],
-    exact eq_zero_or_eq_zero_of_mul_eq_zero this
-  end,
-  ..polynomial.nontrivial,
-  ..polynomial.comm_ring }
+    rw [← leading_coeff_eq_zero, ← leading_coeff_eq_zero],
+    refine eq_zero_or_eq_zero_of_mul_eq_zero _,
+    rw [← leading_coeff_zero, ← leading_coeff_mul, h],
+  end }
 
 lemma nat_degree_mul (hp : p ≠ 0) (hq : q ≠ 0) : nat_degree (p * q) =
   nat_degree p + nat_degree q :=
 by rw [← with_bot.coe_eq_coe, ← degree_eq_nat_degree (mul_ne_zero hp hq),
     with_bot.coe_add, ← degree_eq_nat_degree hp,
     ← degree_eq_nat_degree hq, degree_mul]
 
-lemma nat_trailing_degree_mul (hp : p ≠ 0) (hq : q ≠ 0) :
-  (p * q).nat_trailing_degree = p.nat_trailing_degree + q.nat_trailing_degree :=
-begin
-  simp only [←nat.sub_eq_of_eq_add (nat_degree_eq_reverse_nat_degree_add_nat_trailing_degree _)],
-  rw [reverse_mul_of_domain, nat_degree_mul hp hq, nat_degree_mul (mt reverse_eq_zero.mp hp)
-    (mt reverse_eq_zero.mp hq), reverse_nat_degree, reverse_nat_degree, ←nat.sub_sub, nat.add_comm,
-    nat.add_sub_assoc (nat.sub_le _ _), add_comm, nat.add_sub_assoc (nat.sub_le _ _)],
-end
-
 @[simp] lemma nat_degree_pow (p : polynomial R) (n : ℕ) :
   nat_degree (p ^ n) = n * nat_degree p :=
 if hp0 : p = 0
@@ -102,6 +90,25 @@ begin
   rw [nat_degree_mul h2.1 h2.2], exact nat.le_add_right _ _
 end
 
+end no_zero_divisors
+
+section integral_domain
+variables [integral_domain R] {p q : polynomial R}
+
+instance : integral_domain (polynomial R) :=
+{ ..polynomial.no_zero_divisors,
+  ..polynomial.nontrivial,
+  ..polynomial.comm_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 :=
+begin
+  simp only [←nat.sub_eq_of_eq_add (nat_degree_eq_reverse_nat_degree_add_nat_trailing_degree _)],
+  rw [reverse_mul_of_domain, nat_degree_mul hp hq, nat_degree_mul (mt reverse_eq_zero.mp hp)
+    (mt reverse_eq_zero.mp hq), reverse_nat_degree, reverse_nat_degree, ←nat.sub_sub, nat.add_comm,
+    nat.add_sub_assoc (nat.sub_le _ _), add_comm, nat.add_sub_assoc (nat.sub_le _ _)],
+end
+
 section roots
 
 open multiset