refactor(data/polynomial): extract/add lemmas and golf (#14888)

+ Extract lemmas `roots_multiset_prod_X_sub_C`, `nat_degree_multiset_prod_X_sub_C_eq_card`, `monic_prod_multiset_X_sub_C` from the proof of `C_leading_coeff_mul_prod_multiset_X_sub_C` in *ring_division.lean*.

+ Add the lemma `exists_prod_multiset_X_sub_C_mul` in *ring_division.lean* and `roots_ne_zero_of_splits` in *splitting_field.lean* and use them to golf `nat_degree_eq_card_roots` The proof of the latter originally depends on `eq_prod_roots_of_splits`, but now the dependency reversed, with `nat_degree_eq_card_roots` now used to golf `eq_prod_roots_of_splits` (and `roots_map` as well).

+ Move `prod_multiset_root_eq_finset_root` and `prod_multiset_X_sub_C_dvd` from *field_division.lean* to *ring_division.lean* and golf the proof of the latter, generalizing `field` to `is_domain`.

+ Remove redundant imports and the lemma `exists_multiset_of_splits`, because it is just one direction of `splits_iff_exists_multiset`, and it follows trivially from `eq_prod_roots_of_splits`. It couldn't be removed before this PR because `roots_map` and `eq_prod_roots_of_splits` depended on it.

+ Golf `splits_of_exists_multiset` (independent of other changes).

Author: alreadydone

src/data/polynomial/field_division.lean

@@ -3,11 +3,8 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker
 -/
-import algebra.gcd_monoid.basic
 import data.polynomial.derivative
 import data.polynomial.ring_division
-import data.set.pairwise
-import ring_theory.coprime.lemmas
 import ring_theory.euclidean_domain
 
 /-!
@@ -27,11 +24,6 @@ variables {R : Type u} {S : Type v} {k : Type y} {A : Type z} {a b : R} {n : ℕ
 section is_domain
 variables [comm_ring R] [is_domain R]
 
-lemma prod_multiset_root_eq_finset_root {p : R[X]} :
-  (multiset.map (λ (a : R), X - C a) p.roots).prod =
-  ∏ a in p.roots.to_finset, (X - C a) ^ root_multiplicity a p :=
-by simp only [count_roots, finset.prod_multiset_map_count]
-
 lemma roots_C_mul (p : R[X]) {a : R} (hzero : a ≠ 0) : (C a * p).roots = p.roots :=
 begin
   by_cases hpzero : p = 0,
@@ -490,20 +482,5 @@ begin
   rw [← C_inj, this, C_0],
 end
 
-/-- The product `∏ (X - a)` for `a` inside the multiset `p.roots` divides `p`. -/
-lemma prod_multiset_X_sub_C_dvd (p : R[X]) :
-  (multiset.map (λ (a : R), X - C a) p.roots).prod ∣ p :=
-begin
-  rw prod_multiset_root_eq_finset_root,
-  have hcoprime : pairwise (is_coprime on λ (a : R), polynomial.X - C (id a)) :=
-    pairwise_coprime_X_sub_C function.injective_id,
-  have H : pairwise (is_coprime on λ (a : R), (polynomial.X - C (id a)) ^ (root_multiplicity a p)),
-  { intros a b hdiff, exact (hcoprime a b hdiff).pow },
-  apply finset.prod_dvd_of_coprime (H.set_pairwise (↑(multiset.to_finset p.roots) : set R)),
-  intros a h,
-  rw multiset.mem_to_finset at h,
-  exact pow_root_multiplicity_dvd p a
-end
-
 end field
 end polynomial

src/data/polynomial/ring_division.lean

@@ -463,6 +463,23 @@ lemma roots_prod_X_sub_C (s : finset R) :
 (roots_prod (λ a, X - C a) s (prod_ne_zero_iff.mpr (λ a _, X_sub_C_ne_zero a))).trans
   (by simp_rw [roots_X_sub_C, multiset.bind_singleton, multiset.map_id'])
 
+@[simp] lemma roots_multiset_prod_X_sub_C (s : multiset R) :
+  (s.map (λ a, X - C a)).prod.roots = s :=
+begin
+  rw [roots_multiset_prod, multiset.bind_map],
+  { simp_rw [roots_X_sub_C, multiset.bind_singleton, multiset.map_id'] },
+  { rw [multiset.mem_map], rintro ⟨a, -, h⟩, exact X_sub_C_ne_zero a h },
+end
+
+@[simp] lemma nat_degree_multiset_prod_X_sub_C_eq_card (s : multiset R):
+  (s.map (λ a, X - C a)).prod.nat_degree = s.card :=
+begin
+  rw [nat_degree_multiset_prod_of_monic, multiset.map_map],
+  { convert multiset.sum_repeat 1 _,
+    { convert multiset.map_const _ 1, ext, apply nat_degree_X_sub_C }, { simp } },
+  { intros f hf, obtain ⟨a, ha, rfl⟩ := multiset.mem_map.1 hf, exact monic_X_sub_C a },
+end
+
 lemma card_roots_X_pow_sub_C {n : ℕ} (hn : 0 < n) (a : R) :
   (roots ((X : R[X]) ^ n - C a)).card ≤ n :=
 with_bot.coe_le_coe.1 $
@@ -498,8 +515,8 @@ begin
   simp only [polynomial.map_pow, polynomial.map_sub, map_pow, map_sub, map_X, map_C],
 end
 
-lemma count_map_roots [is_domain A] {p : A[X]} {f : A →+* B} (hf : function.injective f)
-  (a : B) : count a (multiset.map f p.roots) ≤ root_multiplicity a (map f p) :=
+lemma count_map_roots [is_domain A] (p : A[X]) {f : A →+* B} (hf : function.injective f)
+  (a : B) : count a (p.roots.map f) ≤ root_multiplicity a (map f p) :=
 begin
   by_cases h : ∃ t, f t = a,
   { rcases h with ⟨h_w, rfl⟩,
@@ -514,12 +531,12 @@ end
 
 lemma roots_map_of_injective_card_eq_total_degree [is_domain A] [is_domain B] {p : A[X]}
   {f : A →+* B} (hf : function.injective f) (hroots : p.roots.card = p.nat_degree) :
-  multiset.map f p.roots = (map f p).roots :=
+  p.roots.map f = (map f p).roots :=
 begin
   by_cases hp0 : p = 0, { simp only [hp0, roots_zero, multiset.map_zero, polynomial.map_zero], },
   have hmap : map f p ≠ 0, { simpa only [polynomial.map_zero] using (map_injective f hf).ne hp0, },
   apply multiset.eq_of_le_of_card_le,
-  { simpa only [multiset.le_iff_count, count_roots] using count_map_roots hf },
+  { simpa only [multiset.le_iff_count, count_roots] using count_map_roots p hf },
   { simpa only [multiset.card_map, hroots] using (card_roots' _).trans (nat_degree_map_le f p) },
 end
 
@@ -719,8 +736,7 @@ begin
   rw [hr, nat_degree_mul'] at hdeg, swap,
   { rw [hp.leading_coeff, one_mul, leading_coeff_ne_zero], exact rzero },
   rw [mul_comm, @eq_C_of_nat_degree_eq_zero _ _ r] at hr,
-  { convert hr, convert leading_coeff_C _ using 1,
-    rw [hr, leading_coeff_mul_monic hp] },
+  { convert hr, convert leading_coeff_C _ using 1, rw [hr, leading_coeff_mul_monic hp] },
   { exact (add_right_inj _).1 (le_antisymm hdeg $ nat.le.intro rfl) },
 end
 
@@ -741,33 +757,56 @@ theorem pairwise_coprime_X_sub_C {K} [field K] {I : Type v} {s : I → K}
   (H : function.injective s) : pairwise (is_coprime on (λ i : I, X - C (s i))) :=
 λ i j hij, is_coprime_X_sub_C_of_is_unit_sub (sub_ne_zero_of_ne $ H.ne hij).is_unit
 
+lemma monic_prod_multiset_X_sub_C : monic (p.roots.map (λ a, X - C a)).prod :=
+monic_multiset_prod_of_monic _ _ (λ a _, monic_X_sub_C a)
+
+lemma prod_multiset_root_eq_finset_root :
+  (p.roots.map (λ a, X - C a)).prod =
+  p.roots.to_finset.prod (λ a, (X - C a) ^ root_multiplicity a p) :=
+by simp only [count_roots, finset.prod_multiset_map_count]
+
+/-- The product `∏ (X - a)` for `a` inside the multiset `p.roots` divides `p`. -/
+lemma prod_multiset_X_sub_C_dvd (p : R[X]) : (p.roots.map (λ a, X - C a)).prod ∣ p :=
+begin
+  rw ← map_dvd_map _ (is_fraction_ring.injective R $ fraction_ring R) monic_prod_multiset_X_sub_C,
+  rw [prod_multiset_root_eq_finset_root, polynomial.map_prod],
+  refine finset.prod_dvd_of_coprime (λ a _ b _ h, _) (λ a _, _),
+  { simp_rw [polynomial.map_pow, polynomial.map_sub, map_C, map_X],
+    exact (pairwise_coprime_X_sub_C (is_fraction_ring.injective R $ fraction_ring R) _ _ h).pow },
+  { exact polynomial.map_dvd _ (pow_root_multiplicity_dvd p a) },
+end
+
+lemma exists_prod_multiset_X_sub_C_mul (p : R[X]) : ∃ q,
+  (p.roots.map (λ a, X - C a)).prod * q = p ∧
+  p.roots.card + q.nat_degree = p.nat_degree ∧
+  q.roots = 0 :=
+begin
+  obtain ⟨q, he⟩ := prod_multiset_X_sub_C_dvd p,
+  use [q, he.symm],
+  obtain (rfl|hq) := eq_or_ne q 0,
+  { rw mul_zero at he, subst he, simp },
+  split,
+  { conv_rhs { rw he },
+    rw [monic_prod_multiset_X_sub_C.nat_degree_mul' hq, nat_degree_multiset_prod_X_sub_C_eq_card] },
+  { replace he := congr_arg roots he.symm,
+    rw [roots_mul, roots_multiset_prod_X_sub_C] at he,
+    exacts [add_right_eq_self.1 he, mul_ne_zero monic_prod_multiset_X_sub_C.ne_zero hq] },
+end
+
 /-- A polynomial `p` that has as many roots as its degree
 can be written `p = p.leading_coeff * ∏(X - a)`, for `a` in `p.roots`. -/
 lemma C_leading_coeff_mul_prod_multiset_X_sub_C (hroots : p.roots.card = p.nat_degree) :
-  C p.leading_coeff * (p.roots.map (λ (a : R), X - C a)).prod = p :=
-begin
-  symmetry, classical,
-  apply eq_leading_coeff_mul_of_monic_of_dvd_of_nat_degree_le,
-  { exact monic_multiset_prod_of_monic _ _ (λ a _, monic_X_sub_C a) },
-  { rw ← map_dvd_map _ (is_fraction_ring.injective R $ fraction_ring R),
-    swap, { exact monic_multiset_prod_of_monic _ _ (λ a _, monic_X_sub_C a) },
-    rw [finset.prod_multiset_map_count, polynomial.map_prod],
-    refine finset.prod_dvd_of_coprime (λ a _ b _ h, _) (λ a _, _),
-    { simp_rw [polynomial.map_pow, polynomial.map_sub, map_C, map_X],
-      exact (pairwise_coprime_X_sub_C (is_fraction_ring.injective R $ fraction_ring R) _ _ h).pow },
-    { rw count_roots, exact polynomial.map_dvd _ (pow_root_multiplicity_dvd p a) } },
-  { rw [nat_degree_multiset_prod_of_monic, multiset.map_map],
-    { convert hroots.symm.le, convert multiset.sum_repeat 1 _,
-      { convert multiset.map_const _ 1, ext, apply nat_degree_X_sub_C }, { simp } },
-    { intros f hf, obtain ⟨a, ha, rfl⟩ := multiset.mem_map.1 hf, exact monic_X_sub_C a } },
-end
+  C p.leading_coeff * (p.roots.map (λ a, X - C a)).prod = p :=
+(eq_leading_coeff_mul_of_monic_of_dvd_of_nat_degree_le monic_prod_multiset_X_sub_C
+  (prod_multiset_X_sub_C_dvd p) $
+  ((nat_degree_multiset_prod_X_sub_C_eq_card _).trans hroots).ge).symm
 
 /-- A monic polynomial `p` that has as many roots as its degree
 can be written `p = ∏(X - a)`, for `a` in `p.roots`. -/
 lemma prod_multiset_X_sub_C_of_monic_of_roots_card_eq
   (hp : p.monic) (hroots : p.roots.card = p.nat_degree) :
-  (p.roots.map (λ (a : R), X - C a)).prod = p :=
-by {convert C_leading_coeff_mul_prod_multiset_X_sub_C hroots, rw [hp.leading_coeff, C_1, one_mul] }
+  (p.roots.map (λ a, X - C a)).prod = p :=
+by { convert C_leading_coeff_mul_prod_multiset_X_sub_C hroots, rw [hp.leading_coeff, C_1, one_mul] }
 
 end comm_ring
 
@@ -776,7 +815,7 @@ section
 variables [semiring R] [comm_ring S] [is_domain S] (φ : R →+* S)
 
 lemma is_unit_of_is_unit_leading_coeff_of_is_unit_map
-  (f : R[X]) (hf : is_unit (leading_coeff f)) (H : is_unit (map φ f)) :
+  {f : R[X]} (hf : is_unit f.leading_coeff) (H : is_unit (map φ f)) :
   is_unit f :=
 begin
   have dz := degree_eq_zero_of_is_unit H,

src/field_theory/abel_ruffini.lean

@@ -311,7 +311,7 @@ begin
       (minpoly.dvd F α (by rw [aeval_comp, aeval_X_pow, minpoly.aeval]))⟩ },
   { refine gal_is_solvable_tower p (p.comp (X ^ n)) _ hα _,
     { exact gal.splits_in_splitting_field_of_comp _ _ (by rwa [nat_degree_X_pow]) },
-    { obtain ⟨s, hs⟩ := exists_multiset_of_splits _ (splitting_field.splits p),
+    { obtain ⟨s, hs⟩ := (splits_iff_exists_multiset _).1 (splitting_field.splits p),
       rw [map_comp, polynomial.map_pow, map_X, hs, mul_comp, C_comp],
       apply gal_mul_is_solvable (gal_C_is_solvable _),
       rw multiset_prod_comp,

src/field_theory/separable.lean

@@ -404,11 +404,9 @@ end
 
 lemma exists_finset_of_splits
   (i : F →+* K) {f : F[X]} (sep : separable f) (sp : splits i f) :
-  ∃ (s : finset K), f.map i =
-    C (i f.leading_coeff) * (s.prod (λ a : K, (X : K[X]) - C a)) :=
+  ∃ (s : finset K), f.map i = C (i f.leading_coeff) * (s.prod (λ a : K, X - C a)) :=
 begin
-  classical,
-  obtain ⟨s, h⟩ := exists_multiset_of_splits i sp,
+  obtain ⟨s, h⟩ := (splits_iff_exists_multiset _).1 sp,
   use s.to_finset,
   rw [h, finset.prod_eq_multiset_prod, ←multiset.to_finset_eq],
   apply nodup_of_separable_prod,