Cubic normal forms and the elementary symmetric functions of the roots of a split cubic

A polynomial of degree at most three is C a * X ^ 3 + C b * X ^ 2 + C c * X + C d for its own coefficients; this is the inverse half of Mathlib's Cubic.equiv, stated for the polynomial itself rather than its degree-bounded subtype.

A product (X - a)(X - b)(X - c) of three monic linear factors determines the elementary symmetric functions of a, b, c: by Vieta's formulas they are, up to sign, its coefficients. This file records the resulting comparison of two such factorisations over any commutative ring, using Mathlib's expansion Cubic.prod_X_sub_C_eq.

Main results

• Polynomial.eq_cubic_of_natDegree_le_three and Polynomial.Monic.eq_X_pow_three_add: the normal form a * X ^ 3 + b * X ^ 2 + c * X + d of a polynomial of degree at most three, and X ^ 3 + a * X ^ 2 + b * X + c of a monic cubic.
• TauCeti.Polynomial.add_add_eq_and_mul_add_mul_add_mul_eq: if (X - a)(X - b)(X - c) = (X - a')(X - b')(X - c'), then a + b + c = a' + b' + c' and ab + ac + bc = a'b' + a'c' + b'c'.

theorem Polynomial.eq_cubic_of_natDegree_le_three {R : Type u_1} [Semiring R] {p : Polynomial R} (h : p.natDegree ≤ 3) : p = C (p.coeff 3) * X ^ 3 + C (p.coeff 2) * X ^ 2 + C (p.coeff 1) * X + C (p.coeff 0)

A polynomial of degree at most three is C a * X ^ 3 + C b * X ^ 2 + C c * X + C d for its own coefficients a, b, c, d.

theorem Polynomial.Monic.eq_X_pow_three_add {R : Type u_1} [Semiring R] {g : Polynomial R} (hmonic : g.Monic) (hdeg : g.natDegree = 3) : g = X ^ 3 + C (g.coeff 2) * X ^ 2 + C (g.coeff 1) * X + C (g.coeff 0)

A monic polynomial of degree three is X ^ 3 + C a * X ^ 2 + C b * X + C c for its own coefficients a, b, c.

theorem TauCeti.Polynomial.add_add_eq_and_mul_add_mul_add_mul_eq {R : Type u_1} [CommRing R] {a b c a' b' c' : R} (h : (Polynomial.X - Polynomial.C a) * (Polynomial.X - Polynomial.C b) * (Polynomial.X - Polynomial.C c) = (Polynomial.X - Polynomial.C a') * (Polynomial.X - Polynomial.C b') * (Polynomial.X - Polynomial.C c')) : a + b + c = a' + b' + c' ∧ a * b + a * c + b * c = a' * b' + a' * c' + b' * c'

Equal products of three monic linear factors have the same first and second elementary symmetric functions of their roots.