feat: port RingTheory.Polynomial.Vieta (#3137)

Co-authored-by: Matthew Ballard <matt@mrb.email>

Mathlib.lean

@@ -1389,6 +1389,7 @@ import Mathlib.RingTheory.Polynomial.Opposites
 import Mathlib.RingTheory.Polynomial.Pochhammer
 import Mathlib.RingTheory.Polynomial.ScaleRoots
 import Mathlib.RingTheory.Polynomial.Tower
+import Mathlib.RingTheory.Polynomial.Vieta
 import Mathlib.RingTheory.Prime
 import Mathlib.RingTheory.PrincipalIdealDomain
 import Mathlib.RingTheory.RingInvo

Mathlib/Data/Polynomial/RingDivision.lean

@@ -1122,19 +1122,19 @@ set_option linter.uppercaseLean3 false in
 
 /-- A polynomial `p` that has as many roots as its degree
 can be written `p = p.leadingCoeff * ∏(X - a)`, for `a` in `p.roots`. -/
-theorem c_leadingCoeff_mul_prod_multiset_X_sub_C (hroots : Multiset.card p.roots = p.natDegree) :
+theorem C_leadingCoeff_mul_prod_multiset_X_sub_C (hroots : Multiset.card p.roots = p.natDegree) :
     C p.leadingCoeff * (p.roots.map fun a => X - C a).prod = p :=
   (eq_leadingCoeff_mul_of_monic_of_dvd_of_natDegree_le monic_prod_multiset_X_sub_C
       p.prod_multiset_X_sub_C_dvd
       ((natDegree_multiset_prod_X_sub_C_eq_card _).trans hroots).ge).symm
 set_option linter.uppercaseLean3 false in
-#align polynomial.C_leading_coeff_mul_prod_multiset_X_sub_C Polynomial.c_leadingCoeff_mul_prod_multiset_X_sub_C
+#align polynomial.C_leading_coeff_mul_prod_multiset_X_sub_C Polynomial.C_leadingCoeff_mul_prod_multiset_X_sub_C
 
 /-- A monic polynomial `p` that has as many roots as its degree
 can be written `p = ∏(X - a)`, for `a` in `p.roots`. -/
 theorem prod_multiset_X_sub_C_of_monic_of_roots_card_eq (hp : p.Monic)
     (hroots : Multiset.card p.roots = p.natDegree) : (p.roots.map fun a => X - C a).prod = p := by
-  convert c_leadingCoeff_mul_prod_multiset_X_sub_C hroots
+  convert C_leadingCoeff_mul_prod_multiset_X_sub_C hroots
   rw [hp.leadingCoeff, C_1, one_mul]
 set_option linter.uppercaseLean3 false in
 #align polynomial.prod_multiset_X_sub_C_of_monic_of_roots_card_eq Polynomial.prod_multiset_X_sub_C_of_monic_of_roots_card_eq

Mathlib/Data/Polynomial/Splits.lean

@@ -362,7 +362,7 @@ theorem adjoin_rootSet_eq_range [Algebra F K] [Algebra F L] {p : F[X]}
 theorem eq_prod_roots_of_splits {p : K[X]} {i : K →+* L} (hsplit : Splits i p) :
     p.map i = C (i p.leadingCoeff) * ((p.map i).roots.map fun a => X - C a).prod := by
   rw [← leadingCoeff_map]; symm
-  apply c_leadingCoeff_mul_prod_multiset_X_sub_C
+  apply C_leadingCoeff_mul_prod_multiset_X_sub_C
   rw [natDegree_map]; exact (natDegree_eq_card_roots hsplit).symm
 #align polynomial.eq_prod_roots_of_splits Polynomial.eq_prod_roots_of_splits
 
@@ -462,7 +462,7 @@ theorem splits_iff_card_roots {p : K[X]} :
     rw [splits_iff_exists_multiset (RingHom.id K)]
     use p.roots
     simp only [RingHom.id_apply, map_id]
-    exact (c_leadingCoeff_mul_prod_multiset_X_sub_C hroots).symm
+    exact (C_leadingCoeff_mul_prod_multiset_X_sub_C hroots).symm
 #align polynomial.splits_iff_card_roots Polynomial.splits_iff_card_roots
 
 theorem aeval_root_derivative_of_splits [Algebra K L] {P : K[X]} (hmo : P.Monic)

Mathlib/RingTheory/Polynomial/Vieta.lean

@@ -0,0 +1,198 @@
+/-
+Copyright (c) 2020 Hanting Zhang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Hanting Zhang
+
+! This file was ported from Lean 3 source module ring_theory.polynomial.vieta
+! leanprover-community/mathlib commit f694c7dead66f5d4c80f446c796a5aad14707f0e
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Data.Polynomial.Splits
+import Mathlib.RingTheory.MvPolynomial.Symmetric
+
+/-!
+# Vieta's Formula
+
+The main result is `Multiset.prod_X_add_C_eq_sum_esymm`, which shows that the product of
+linear terms `X + λ` with `λ` in a `Multiset s` is equal to a linear combination of the
+symmetric functions `esymm s`.
+
+From this, we deduce `MvPolynomial.prod_X_add_C_eq_sum_esymm` which is the equivalent formula
+for the product of linear terms `X + X i` with `i` in a `Fintype σ` as a linear combination
+of the symmetric polynomials `esymm σ R j`.
+
+For `R` be an integral domain (so that `p.roots` is defined for any `p : R[X]` as a multiset),
+we derive `Polynomial.coeff_eq_esymm_roots_of_card`, the relationship between the coefficients and
+the roots of `p` for a polynomial `p` that splits (i.e. having as many roots as its degree).
+-/
+
+
+open BigOperators Polynomial
+
+namespace Multiset
+
+open Polynomial
+
+section Semiring
+
+variable {R : Type _} [CommSemiring R]
+
+/-- A sum version of Vieta's formula for `multiset`: the product of the linear terms `X + λ` where
+`λ` runs through a multiset `s` is equal to a linear combination of the symmetric functions
+`esymm s` of the `λ`'s .-/
+theorem prod_X_add_C_eq_sum_esymm (s : Multiset R) :
+    (s.map fun r => X + C r).prod =
+      ∑ j in Finset.range (Multiset.card s + 1), (C (s.esymm j) * X ^ (Multiset.card s - j)) := by
+  classical
+    rw [prod_map_add, antidiagonal_eq_map_powerset, map_map, ← bind_powerset_len,
+      map_bind, sum_bind, Finset.sum_eq_multiset_sum, Finset.range_val, map_congr (Eq.refl _)]
+    intro _ _
+    rw [esymm, ← sum_hom', ← sum_map_mul_right, map_congr (Eq.refl _)]
+    intro s ht
+    rw [mem_powersetLen] at ht
+    dsimp
+    rw [prod_hom' s (Polynomial.C : R →+* R[X])]
+    simp [ht, map_const, prod_replicate, prod_hom', map_id', card_sub]
+set_option linter.uppercaseLean3 false in
+#align multiset.prod_X_add_C_eq_sum_esymm Multiset.prod_X_add_C_eq_sum_esymm
+
+/-- Vieta's formula for the coefficients of the product of linear terms `X + λ` where `λ` runs
+through a multiset `s` : the `k`th coefficient is the symmetric function `esymm (card s - k) s`. -/
+theorem prod_X_add_C_coeff (s : Multiset R) {k : ℕ} (h : k ≤ Multiset.card s) :
+    (s.map fun r => X + C r).prod.coeff k = s.esymm (Multiset.card s - k) := by
+  convert Polynomial.ext_iff.mp (prod_X_add_C_eq_sum_esymm s) k using 1
+  simp_rw [finset_sum_coeff, coeff_C_mul_X_pow]
+  rw [Finset.sum_eq_single_of_mem (Multiset.card s - k) _]
+  · rw [if_pos (Nat.sub_sub_self h).symm]
+  · intro j hj1 hj2
+    suffices k ≠ card s - j by rw [if_neg this]
+    · intro hn
+      rw [hn, Nat.sub_sub_self (Nat.lt_succ_iff.mp (Finset.mem_range.mp hj1))] at hj2
+      exact Ne.irrefl hj2
+  · rw [Finset.mem_range]
+    exact Nat.sub_lt_succ (Multiset.card s) k
+set_option linter.uppercaseLean3 false in
+#align multiset.prod_X_add_C_coeff Multiset.prod_X_add_C_coeff
+
+theorem prod_X_add_C_coeff' {σ} (s : Multiset σ) (r : σ → R) {k : ℕ} (h : k ≤ Multiset.card s) :
+    (s.map fun i => X + C (r i)).prod.coeff k = (s.map r).esymm (Multiset.card s - k) := by
+  erw [← map_map (fun r => X + C r) r, prod_X_add_C_coeff] <;> rw [s.card_map r]; assumption
+set_option linter.uppercaseLean3 false in
+#align multiset.prod_X_add_C_coeff' Multiset.prod_X_add_C_coeff'
+
+theorem _root_.Finset.prod_X_add_C_coeff {σ} (s : Finset σ) (r : σ → R) {k : ℕ} (h : k ≤ s.card) :
+    (∏ i in s, (X + C (r i))).coeff k = ∑ t in s.powersetLen (s.card - k), ∏ i in t, r i := by
+  rw [Finset.prod, prod_X_add_C_coeff' _ r h, Multiset.Finset.esymm_map_val]
+  rfl
+set_option linter.uppercaseLean3 false in
+#align finset.prod_X_add_C_coeff Finset.prod_X_add_C_coeff
+
+end Semiring
+
+section Ring
+
+variable {R : Type _} [CommRing R]
+
+theorem esymm_neg (s : Multiset R) (k : ℕ) : (map Neg.neg s).esymm k = (-1) ^ k * esymm s k := by
+  rw [esymm, esymm, ← Multiset.sum_map_mul_left, Multiset.powersetLen_map, Multiset.map_map,
+    map_congr (Eq.refl _)]
+  intro x hx
+  rw [(mem_powersetLen.mp hx).right.symm, ← prod_replicate, ← Multiset.map_const]
+  nth_rw 3 [← map_id' x]
+  rw [← prod_map_mul, map_congr (Eq.refl _)];rfl
+  exact fun z _ => neg_one_mul z
+#align multiset.esymm_neg Multiset.esymm_neg
+
+theorem prod_X_sub_X_eq_sum_esymm (s : Multiset R) :
+    (s.map fun t => X - C t).prod =
+      ∑ j in Finset.range (Multiset.card s + 1), (-1) ^ j * (C (s.esymm j) *
+      X ^ (Multiset.card s - j)) := by
+  conv_lhs =>
+    congr
+    congr
+    ext x
+    rw [sub_eq_add_neg]
+    rw [← map_neg C x]
+  convert prod_X_add_C_eq_sum_esymm (map (fun t => -t) s) using 1
+  · rw [map_map]; rfl
+  · simp only [esymm_neg, card_map, mul_assoc, map_mul, map_pow, map_neg, map_one]
+set_option linter.uppercaseLean3 false in
+#align multiset.prod_X_sub_C_eq_sum_esymm Multiset.prod_X_sub_X_eq_sum_esymm
+
+theorem prod_X_sub_C_coeff (s : Multiset R) {k : ℕ} (h : k ≤ Multiset.card s) :
+    (s.map fun t => X - C t).prod.coeff k =
+    (-1) ^ (Multiset.card s - k) * s.esymm (Multiset.card s - k) := by
+  conv_lhs =>
+    congr
+    congr
+    congr
+    ext x
+    rw [sub_eq_add_neg]
+    rw [← map_neg C x]
+  convert prod_X_add_C_coeff (map (fun t => -t) s) _ using 1
+  · rw [map_map]; rfl
+  · rw [esymm_neg, card_map]
+  · rwa [card_map]
+set_option linter.uppercaseLean3 false in
+#align multiset.prod_X_sub_C_coeff Multiset.prod_X_sub_C_coeff
+
+/-- Vieta's formula for the coefficients and the roots of a polynomial over an integral domain
+  with as many roots as its degree. -/
+theorem _root_.Polynomial.coeff_eq_esymm_roots_of_card [IsDomain R] {p : R[X]}
+    (hroots : Multiset.card p.roots = p.natDegree) {k : ℕ} (h : k ≤ p.natDegree) :
+    p.coeff k = p.leadingCoeff * (-1) ^ (p.natDegree - k) * p.roots.esymm (p.natDegree - k) := by
+  conv_lhs => rw [← C_leadingCoeff_mul_prod_multiset_X_sub_C hroots]
+  rw [coeff_C_mul, mul_assoc]; congr
+  have : k ≤ card (roots p) := by rw [hroots]; exact h
+  convert p.roots.prod_X_sub_C_coeff this using 3 <;> rw [hroots]
+#align polynomial.coeff_eq_esymm_roots_of_card Polynomial.coeff_eq_esymm_roots_of_card
+
+/-- Vieta's formula for split polynomials over a field. -/
+theorem _root_.Polynomial.coeff_eq_esymm_roots_of_splits {F} [Field F] {p : F[X]}
+    (hsplit : p.Splits (RingHom.id F)) {k : ℕ} (h : k ≤ p.natDegree) :
+    p.coeff k = p.leadingCoeff * (-1) ^ (p.natDegree - k) * p.roots.esymm (p.natDegree - k) :=
+  Polynomial.coeff_eq_esymm_roots_of_card (splits_iff_card_roots.1 hsplit) h
+#align polynomial.coeff_eq_esymm_roots_of_splits Polynomial.coeff_eq_esymm_roots_of_splits
+
+end Ring
+
+end Multiset
+
+section MvPolynomial
+
+open Finset Polynomial Fintype
+
+variable (R σ : Type _) [CommSemiring R] [Fintype σ]
+
+/-- A sum version of Vieta's formula for `MvPolynomial`: viewing `X i` as variables,
+the product of linear terms `λ + X i` is equal to a linear combination of
+the symmetric polynomials `esymm σ R j`. -/
+theorem MvPolynomial.prod_C_add_X_eq_sum_esymm :
+    (∏ i : σ, (Polynomial.X + Polynomial.C (MvPolynomial.X i))) =
+      ∑ j in range (card σ + 1), Polynomial.C
+        (MvPolynomial.esymm σ R j) * Polynomial.X ^ (card σ - j) := by
+  let s := Finset.univ.val.map fun i : σ => (MvPolynomial.X i : MvPolynomial σ R)
+  rw [(_ : card σ = Multiset.card s)]
+  · simp_rw [MvPolynomial.esymm_eq_multiset_esymm σ R, Finset.prod_eq_multiset_prod]
+    convert Multiset.prod_X_add_C_eq_sum_esymm s
+    rw [Multiset.map_map]; rfl
+  · rw [Multiset.card_map]
+    rfl
+set_option linter.uppercaseLean3 false in
+#align mv_polynomial.prod_C_add_X_eq_sum_esymm MvPolynomial.prod_C_add_X_eq_sum_esymm
+
+theorem MvPolynomial.prod_X_add_C_coeff (k : ℕ) (h : k ≤ card σ) :
+    (∏ i : σ, (Polynomial.X + Polynomial.C (MvPolynomial.X i)) : Polynomial _).coeff k =
+    MvPolynomial.esymm σ R (card σ - k) := by
+  let s := Finset.univ.val.map fun i => (MvPolynomial.X i : MvPolynomial σ R)
+  rw [(_ : card σ = Multiset.card s)] at h⊢
+  · rw [MvPolynomial.esymm_eq_multiset_esymm σ R, Finset.prod_eq_multiset_prod]
+    convert Multiset.prod_X_add_C_coeff s h
+    dsimp
+    rw [Multiset.map_map]; rfl
+  repeat' rw [Multiset.card_map]; rfl
+set_option linter.uppercaseLean3 false in
+#align mv_polynomial.prod_X_add_C_coeff MvPolynomial.prod_X_add_C_coeff
+
+end MvPolynomial