Symmetric polynomials

Multisets {b₀, …, bₙ₋₁} attached to maps b : Fin n → α and symmetric-function machinery feeding the algebraic estimates of Niven's proof.

def valuesFin {α : Type u_1} {n : ℕ} (b : Fin n → α) : Multiset α

The multiset {b₀, …, bₙ₋₁} attached to b : Fin n → α.

Equations

• valuesFin b = Multiset.map b Finset.univ.val

theorem exists_valuesFin_eq_multiset {α : Type u_1} (s : Multiset α) : ∃ (n : ℕ) (a : Fin n → α), s = valuesFin a

Every multiset can be indexed by a map a : Fin n → α.

theorem exists_valuesFin_eq_aroots (P : Polynomial ℚ) : ∃ (n : ℕ) (a : Fin n → ℂ), P.aroots ℂ = valuesFin a

The roots of a polynomial can be listed as a valuesFin a₀, …, aₙ₋₁.

theorem coeff_eq_esymm_of_roots {R : Type u_1} {S : Type u_2} [CommRing R] [Field S] [Algebra R S] [IsAlgClosed S] {n : ℕ} (B : Polynomial R) (b : Fin n → S) (hmonic : B.Monic) (hroots : B.aroots S = valuesFin b) {k : ℕ} (hk : k ≤ n) : (algebraMap R S) (B.coeff k) = (MvPolynomial.aeval b) ((-1) ^ (n - k) * MvPolynomial.esymm (Fin n) ℤ (n - k))

For a monic polynomial with roots b₀, …, bₙ₋₁, its k-th coefficient is written with an elementary symmetric polynomial in the roots.

theorem symmetric_poly_at_roots_eq_poly_of_esymm {R : Type u_1} {S : Type u_2} [CommRing R] [Field S] [Algebra R S] [IsAlgClosed S] {n : ℕ} (B : Polynomial R) (a : Fin n → S) (hmonic : B.Monic) (hroots : B.aroots S = valuesFin a) (P : MvPolynomial (Fin n) ℤ) (hP : P.IsSymmetric) : ∃ (Q : MvPolynomial (Fin n) ℤ), (MvPolynomial.aeval a) P = (algebraMap R S) ((MvPolynomial.aeval fun (i : Fin n) => (-1) ^ (↑i + 1) * B.coeff (n - (↑i + 1))) Q)

If P is symmetric, then P(b₀, …, bₙ₋₁) can be rewritten as a polynomial expression in the coefficients of the monic polynomial with roots b₀, …, bₙ₋₁.

theorem symmetric_poly_at_roots {R : Type u_1} {S : Type u_2} [CommRing R] [Field S] [Algebra R S] [IsAlgClosed S] {n : ℕ} (B : Polynomial R) (a : Fin n → S) (hmonic : B.Monic) (hroots : B.aroots S = valuesFin a) (P : MvPolynomial (Fin n) ℤ) (hP : P.IsSymmetric) : ∃ (z : R), (MvPolynomial.aeval a) P = (algebraMap R S) z

If P is symmetric, then P(b₀, …, bₙ₋₁) ∈ R if b₀, …, bₙ₋₁ are the roots of a monic polynomial over R.