feat(data/polynomial/ring_division): move lemmas, add lemmas (#16432)

Rename `count_map_roots` to `count_map_roots_of_injective`.

Add 8 lemmas:
```
le_root_multiplicity_iff
root_multiplicity_le_iff
pow_root_multiplicity_not_dvd
_root_.multiset.prod_X_sub_C_dvd_iff_le_roots
count_map_roots
map_roots_le
map_roots_le_of_injective
card_roots_le_map
```

Remove `root_multiplicity_of_dvd`, it's just the left direction of `le_root_multiplicity_iff`.

Move and golf 3 lemmas:
```
le_root_multiplicity_map (8 -> 5)
eq_root_multiplicity_map (10 -> 7)
roots_map_of_injective_card_eq_total_degree (7 -> 4)
```

- [x] depends on: #16440

Co-authored-by: alreadydone <junyanxumath@gmail.com>



Co-authored-by: Junyan Xu <junyanxumath@gmail.com>

Author: astrainfinita

src/data/polynomial/ring_division.lean

@@ -225,7 +225,37 @@ instance : is_domain R[X] :=
 end ring
 
 section comm_ring
-variables [comm_ring R] [is_domain R] {p q : R[X]}
+variable [comm_ring R]
+
+/-- The multiplicity of `a` as root of a nonzero polynomial `p` is at least `n` iff
+  `(X - a) ^ n` divides `p`. -/
+lemma le_root_multiplicity_iff {p : R[X]} (p0 : p ≠ 0) {a : R} {n : ℕ} :
+  n ≤ root_multiplicity a p ↔ (X - C a) ^ n ∣ p :=
+begin
+  simp_rw [root_multiplicity, dif_neg p0, nat.le_find_iff, not_not],
+  refine ⟨λ h, _, λ h m hm, (pow_dvd_pow _ hm).trans h⟩,
+  cases n, { rw pow_zero, apply one_dvd }, { exact h n n.lt_succ_self },
+end
+
+lemma root_multiplicity_le_iff {p : R[X]} (p0 : p ≠ 0) (a : R) (n : ℕ) :
+  root_multiplicity a p ≤ n ↔ ¬ (X - C a) ^ (n + 1) ∣ p :=
+by rw [← (le_root_multiplicity_iff p0).not, not_le, nat.lt_add_one_iff]
+
+lemma pow_root_multiplicity_not_dvd {p : R[X]} (p0 : p ≠ 0) (a : R) :
+  ¬ (X - C a) ^ (root_multiplicity a p + 1) ∣ p :=
+by rw [← root_multiplicity_le_iff p0]
+
+/-- The multiplicity of `p + q` is at least the minimum of the multiplicities. -/
+lemma root_multiplicity_add {p q : R[X]} (a : R) (hzero : p + q ≠ 0) :
+  min (root_multiplicity a p) (root_multiplicity a q) ≤ root_multiplicity a (p + q) :=
+begin
+  rw le_root_multiplicity_iff hzero,
+  have hdivp : (X - C a) ^ root_multiplicity a p ∣ p := pow_root_multiplicity_dvd p a,
+  have hdivq : (X - C a) ^ root_multiplicity a q ∣ q := pow_root_multiplicity_dvd q a,
+  exact min_pow_dvd_add hdivp hdivq
+end
+
+variables [is_domain R] {p q : R[X]}
 
 section roots
 
@@ -315,27 +345,6 @@ begin
   simp only [root_multiplicity_mul hzero, root_multiplicity_X_sub_C_self, hn, nat.one_add]
 end
 
-/-- If `(X - a) ^ n` divides a polynomial `p` then the multiplicity of `a` as root of `p` is at
-least `n`. -/
-lemma root_multiplicity_of_dvd {p : R[X]} {a : R} {n : ℕ}
-  (hzero : p ≠ 0) (h : (X - C a) ^ n ∣ p) : n ≤ root_multiplicity a p :=
-begin
-  obtain ⟨q, hq⟩ := exists_eq_mul_right_of_dvd h,
-  rw hq at hzero,
-  simp only [hq, root_multiplicity_mul hzero, root_multiplicity_X_sub_C_pow,
-             ge_iff_le, _root_.zero_le, le_add_iff_nonneg_right],
-end
-
-/-- The multiplicity of `p + q` is at least the minimum of the multiplicities. -/
-lemma root_multiplicity_add {p q : R[X]} (a : R) (hzero : p + q ≠ 0) :
-  min (root_multiplicity a p) (root_multiplicity a q) ≤ root_multiplicity a (p + q) :=
-begin
-  refine root_multiplicity_of_dvd hzero _,
-  have hdivp : (X - C a) ^ root_multiplicity a p ∣ p := pow_root_multiplicity_dvd p a,
-  have hdivq : (X - C a) ^ root_multiplicity a q ∣ q := pow_root_multiplicity_dvd q a,
-  exact min_pow_dvd_add hdivp hdivq
-end
-
 lemma exists_multiset_roots : ∀ {p : R[X]} (hp : p ≠ 0),
   ∃ s : multiset R, (s.card : with_bot ℕ) ≤ degree p ∧ ∀ a, s.count a = root_multiplicity a p
 | p := λ hp, by haveI := classical.prop_decidable (∃ x, is_root p x); exact
@@ -541,61 +550,6 @@ calc ((roots ((X : R[X]) ^ n - C a)).card : with_bot ℕ)
       ≤ degree ((X : R[X]) ^ n - C a) : card_roots (X_pow_sub_C_ne_zero hn a)
   ... = n : degree_X_pow_sub_C hn a
 
-section
-
-variables {A B : Type*} [comm_ring A] [comm_ring B]
-
-lemma le_root_multiplicity_map {p : A[X]} {f : A →+* B} (hmap : map f p ≠ 0) (a : A) :
-  root_multiplicity a p ≤ root_multiplicity (f a) (map f p) :=
-begin
-  have hp0 : p ≠ 0 := λ h, hmap (h.symm ▸ polynomial.map_zero f),
-  rw [root_multiplicity, root_multiplicity, dif_neg hp0, dif_neg hmap],
-  simp only [not_not, nat.lt_find_iff, nat.le_find_iff],
-  intros m hm,
-  have := (map_ring_hom f).map_dvd (hm m le_rfl),
-  simpa only [coe_map_ring_hom, map_pow, map_sub, map_X, map_C],
-end
-
-lemma eq_root_multiplicity_map {p : A[X]} {f : A →+* B} (hf : function.injective f)
-  (a : A) : root_multiplicity a p = root_multiplicity (f a) (map f p) :=
-begin
-  by_cases hp0 : p = 0, { simp only [hp0, root_multiplicity_zero, polynomial.map_zero], },
-  have hmap : map f p ≠ 0, { simpa only [polynomial.map_zero] using (map_injective f hf).ne hp0, },
-  apply le_antisymm (le_root_multiplicity_map hmap a),
-  rw [root_multiplicity, root_multiplicity, dif_neg hp0, dif_neg hmap],
-  simp only [not_not, nat.lt_find_iff, nat.le_find_iff],
-  intros m hm, rw ← map_dvd_map f hf ((monic_X_sub_C a).pow _),
-  convert hm m le_rfl,
-  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 (p.roots.map f) ≤ root_multiplicity a (map f p) :=
-begin
-  by_cases h : ∃ t, f t = a,
-  { rcases h with ⟨h_w, rfl⟩,
-    rw [multiset.count_map_eq_count' f _ hf, count_roots],
-    exact (eq_root_multiplicity_map hf h_w).le },
-  { suffices : (multiset.map f p.roots).count a = 0,
-    { rw this, exact zero_le _, },
-    rw [multiset.count_map, multiset.card_eq_zero, multiset.filter_eq_nil],
-    rintro k hk rfl,
-    exact h ⟨k, rfl⟩, },
-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) :
-  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 p hf },
-  { simpa only [multiset.card_map, hroots] using (card_roots' _).trans (nat_degree_map_le f p) },
-end
-
-end
-
 section nth_roots
 
 /-- `nth_roots n a` noncomputably returns the solutions to `x ^ n = a`-/
@@ -847,12 +801,21 @@ begin
   { exact polynomial.map_dvd _ (pow_root_multiplicity_dvd p a) },
 end
 
+/-- A Galois connection. -/
+lemma _root_.multiset.prod_X_sub_C_dvd_iff_le_roots {p : R[X]} (hp : p ≠ 0) (s : multiset R) :
+  (s.map (λ a, X - C a)).prod ∣ p ↔ s ≤ p.roots :=
+⟨λ h, multiset.le_iff_count.2 $ λ r, begin
+  rw [count_roots, le_root_multiplicity_iff hp, ← multiset.prod_repeat,
+    ← multiset.map_repeat (λ a, X - C a), ← multiset.filter_eq],
+  exact (multiset.prod_dvd_prod_of_le $ multiset.map_le_map $ s.filter_le _).trans h,
+end, λ h, (multiset.prod_dvd_prod_of_le $ multiset.map_le_map h).trans p.prod_multiset_X_sub_C_dvd⟩
+
 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,
+  obtain ⟨q, he⟩ := p.prod_multiset_X_sub_C_dvd,
   use [q, he.symm],
   obtain (rfl|hq) := eq_or_ne q 0,
   { rw mul_zero at he, subst he, simp },
@@ -869,8 +832,7 @@ 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, 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
+  p.prod_multiset_X_sub_C_dvd ((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`. -/
@@ -881,6 +843,75 @@ by { convert C_leading_coeff_mul_prod_multiset_X_sub_C hroots, rw [hp.leading_co
 
 end comm_ring
 
+section
+variables {A B : Type*} [comm_ring A] [comm_ring B]
+
+lemma le_root_multiplicity_map {p : A[X]} {f : A →+* B} (hmap : map f p ≠ 0) (a : A) :
+  root_multiplicity a p ≤ root_multiplicity (f a) (p.map f) :=
+begin
+  rw [le_root_multiplicity_iff hmap],
+  refine trans _ ((map_ring_hom f).map_dvd (pow_root_multiplicity_dvd p a)),
+  rw [map_pow, map_sub, coe_map_ring_hom, map_X, map_C],
+end
+
+lemma eq_root_multiplicity_map {p : A[X]} {f : A →+* B} (hf : function.injective f)
+  (a : A) : root_multiplicity a p = root_multiplicity (f a) (p.map f) :=
+begin
+  by_cases hp0 : p = 0, { simp only [hp0, root_multiplicity_zero, polynomial.map_zero], },
+  apply le_antisymm (le_root_multiplicity_map ((polynomial.map_ne_zero_iff hf).mpr hp0) a),
+  rw [le_root_multiplicity_iff hp0, ← map_dvd_map f hf ((monic_X_sub_C a).pow _),
+    polynomial.map_pow, polynomial.map_sub, map_X, map_C],
+  apply pow_root_multiplicity_dvd,
+end
+
+lemma count_map_roots [is_domain A] {p : A[X]} {f : A →+* B} (hmap : map f p ≠ 0) (b : B) :
+  (p.roots.map f).count b ≤ root_multiplicity b (p.map f) :=
+begin
+  rw [le_root_multiplicity_iff hmap, ← multiset.prod_repeat, ← multiset.map_repeat (λ a, X - C a)],
+  rw ← multiset.filter_eq,
+  refine (multiset.prod_dvd_prod_of_le $ multiset.map_le_map $ multiset.filter_le _ _).trans _,
+  convert polynomial.map_dvd _ p.prod_multiset_X_sub_C_dvd,
+  simp only [polynomial.map_multiset_prod, multiset.map_map],
+  congr, ext1,
+  simp only [function.comp_app, polynomial.map_sub, map_X, map_C],
+end
+
+lemma count_map_roots_of_injective [is_domain A] (p : A[X]) {f : A →+* B}
+  (hf : function.injective f) (b : B) :
+  (p.roots.map f).count b ≤ root_multiplicity b (p.map f) :=
+begin
+  by_cases hp0 : p = 0,
+  { simp only [hp0, roots_zero, multiset.map_zero,
+      multiset.count_zero, polynomial.map_zero, root_multiplicity_zero] },
+  { exact count_map_roots ((polynomial.map_ne_zero_iff hf).mpr hp0) b },
+end
+
+lemma map_roots_le [is_domain A] [is_domain B] {p : A[X]} {f : A →+* B} (h : p.map f ≠ 0) :
+  p.roots.map f ≤ (p.map f).roots :=
+multiset.le_iff_count.2 $ λ b, by { rw count_roots, apply count_map_roots h }
+
+lemma map_roots_le_of_injective [is_domain A] [is_domain B] (p : A[X])
+  {f : A →+* B} (hf : function.injective f) :
+  p.roots.map f ≤ (p.map f).roots :=
+begin
+  by_cases hp0 : p = 0, { simp only [hp0, roots_zero, multiset.map_zero, polynomial.map_zero], },
+  exact map_roots_le ((polynomial.map_ne_zero_iff hf).mpr hp0),
+end
+
+lemma card_roots_le_map [is_domain A] [is_domain B] {p : A[X]} {f : A →+* B} (h : p.map f ≠ 0) :
+  p.roots.card ≤ (p.map f).roots.card :=
+by { rw ← p.roots.card_map f, exact multiset.card_le_of_le (map_roots_le h) }
+
+lemma roots_map_of_injective_of_card_eq_nat_degree [is_domain A] [is_domain B] {p : A[X]}
+  {f : A →+* B} (hf : function.injective f) (hroots : p.roots.card = p.nat_degree) :
+  p.roots.map f = (p.map f).roots :=
+begin
+  apply multiset.eq_of_le_of_card_le (map_roots_le_of_injective p hf),
+  simpa only [multiset.card_map, hroots] using (card_roots' _).trans (nat_degree_map_le f p),
+end
+
+end
+
 section
 
 variables [semiring R] [comm_ring S] [is_domain S] (φ : R →+* S)

src/field_theory/splitting_field.lean

@@ -273,7 +273,7 @@ by rw [degree_eq_nat_degree p_ne_zero, nat_degree_eq_card_roots hsplit]
 
 theorem roots_map {f : K[X]} (hf : f.splits $ ring_hom.id K) :
   (f.map i).roots = f.roots.map i :=
-(roots_map_of_injective_card_eq_total_degree i.injective $
+(roots_map_of_injective_of_card_eq_nat_degree i.injective $
   by { convert (nat_degree_eq_card_roots hf).symm, rw map_id }).symm
 
 lemma image_root_set [algebra F K] [algebra F L] {p : F[X]} (h : p.splits (algebra_map F K))