Resultant of two polynomials

This file contains basic facts about resultant of two polynomials over commutative rings.

Main definitions

• Polynomial.resultant: The resultant of two polynomials p and q is defined as the determinant of the Sylvester matrix of p and q.
• Polynomial.discr: The discriminant of a polynomial f is defined as the resultant of f and f.derivative, modified by factoring out a sign and a power of the leading term.

TODO

• The eventual goal is to prove the following property: resultant (∏ a ∈ s, (X - C a)) f = ∏ a ∈ s, f.eval a. This allows us to write the resultant f g as the product of terms of the form a - b where a is a root of f and b is a root of g.
• A smaller intermediate goal is to show that the Sylvester matrix corresponds to the linear map that we will call the Sylvester map, which is R[X]_n × R[X]_m →ₗ[R] R[X]_(n + m) given by (p, q) ↦ f * p + g * q, where R[X]_n is Polynomial.degreeLT in Mathlib.RingTheory.Polynomial.Basic.
• Resultant of two binary forms (i.e. homogeneous polynomials in two variables), after binary forms are implemented.

def Polynomial.sylvester {R : Type u_1} [Semiring R] (f g : Polynomial R) (m n : ℕ) : Matrix (Fin (m + n)) (Fin (m + n)) R

The Sylvester matrix of two polynomials f and g of degrees m and n respectively is a (m+n) × (m+n) matrix with the coefficients of f and g arranged in a specific way. Here, m and n are free variables, not necessarily equal to the actual degrees of the polynomials f and g.

Note that the natural definition would be a Matrix (Fin (m + n)) (Fin m ⊕ Fin n) R but we prefer having this as a square matrix to take determinants later on.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Polynomial.sylvester_zero_left_deg {R : Type u_1} [Semiring R] (f g : Polynomial R) (m : ℕ) : f.sylvester g 0 m = Matrix.diagonal fun (x : Fin (0 + m)) => f.coeff 0

theorem Polynomial.sylvester_comm {R : Type u_1} [Semiring R] (f g : Polynomial R) (m n : ℕ) : f.sylvester g m n = (Matrix.reindex (finCongr ⋯) (finSumFinEquiv.symm.trans ((Equiv.sumComm (Fin n) (Fin m)).trans finSumFinEquiv))) (g.sylvester f n m)

theorem Polynomial.sylvester_map_map {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f g : Polynomial R) (m n : ℕ) (φ : R →+* S) : (map φ f).sylvester (map φ g) m n = φ.mapMatrix (f.sylvester g m n)

noncomputable def Polynomial.sylvesterDeriv {R : Type u_1} [Semiring R] (f : Polynomial R) : Matrix (Fin (f.natDegree - 1 + f.natDegree)) (Fin (f.natDegree - 1 + f.natDegree)) R

The Sylvester matrix for f and f.derivative, modified by dividing the bottom row by the leading coefficient of f. Important because its determinant is (up to a sign) the discriminant of f.

Equations

• One or more equations did not get rendered due to their size.

theorem Polynomial.sylvesterDeriv_updateRow {R : Type u_1} [Semiring R] (f : Polynomial R) (hf : 0 < f.natDegree) : f.sylvesterDeriv.updateRow ⟨2 * f.natDegree - 2, ⋯⟩ (f.leadingCoeff • f.sylvesterDeriv ⟨2 * f.natDegree - 2, ⋯⟩) = (derivative f).sylvester f (f.natDegree - 1) f.natDegree

We can get the usual Sylvester matrix of f and f.derivative back from the modified one by multiplying the last row by the leading coefficient of f.

def Polynomial.resultant {R : Type u_1} [CommRing R] (f g : Polynomial R) (m : ℕ := f.natDegree) (n : ℕ := g.natDegree) : R

The resultant of two polynomials f and g is the determinant of the Sylvester matrix of f and g. The size arguments m and n are implemented as optParam, meaning that the default values are f.natDegree and g.natDegree respectively, but they can also be specified to be other values.

Equations

• f.resultant g m n = (f.sylvester g m n).det

@[simp]

theorem Polynomial.resultant_map_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f g : Polynomial R) (m n : ℕ) (φ : R →+* S) : (map φ f).resultant (map φ g) m n = φ (f.resultant g m n)

@[simp]

theorem Polynomial.resultant_zero_left_deg {R : Type u_1} [CommRing R] (f g : Polynomial R) (m : ℕ) : f.resultant g 0 m = f.coeff 0 ^ m

theorem Polynomial.resultant_C_zero_left {R : Type u_1} [CommRing R] (g : Polynomial R) (r : R) (m : ℕ) : (C r).resultant g 0 m = r ^ m

For polynomial f and constant a, Res(f, a) = a ^ m.

theorem Polynomial.resultant_comm {R : Type u_1} [CommRing R] (f g : Polynomial R) (m n : ℕ) : f.resultant g m n = (-1) ^ (m * n) * g.resultant f n m

Res(f, g) = (-1)ᵐⁿ Res(g, f)

@[simp]

theorem Polynomial.resultant_zero_right_deg {R : Type u_1} [CommRing R] (f g : Polynomial R) (m : ℕ) : f.resultant g m 0 = g.coeff 0 ^ m

theorem Polynomial.resultant_C_zero_right {R : Type u_1} [CommRing R] (f : Polynomial R) (m : ℕ) (r : R) : f.resultant (C r) m 0 = r ^ m

Res(a, g) = a ^ deg g

@[simp]

theorem Polynomial.resultant_zero_right {R : Type u_1} [CommRing R] (f : Polynomial R) (m n : ℕ) : f.resultant 0 m n = 0 ^ m * f.coeff 0 ^ n

@[simp]

theorem Polynomial.resultant_zero_left {R : Type u_1} [CommRing R] (g : Polynomial R) (m n : ℕ) : resultant 0 g m n = 0 ^ n * g.coeff 0 ^ m

theorem Polynomial.resultant_zero_zero {R : Type u_1} [CommRing R] (m n : ℕ) : resultant 0 0 m n = 0 ^ (m + n)

theorem Polynomial.resultant_add_mul_right {R : Type u_1} [CommRing R] (f g p : Polynomial R) (m n : ℕ) (hp : p.natDegree + m ≤ n) (hf : f.natDegree ≤ m) : f.resultant (g + f * p) m n = f.resultant g m n

Res(f, g + fp) = Res(f, g) if deg f + deg p ≤ deg g.

theorem Polynomial.resultant_add_mul_left {R : Type u_1} [CommRing R] (f g p : Polynomial R) (m n : ℕ) (hk : p.natDegree + n ≤ m) (hg : g.natDegree ≤ n) : (f + g * p).resultant g m n = f.resultant g m n

Res(f + gp, g) = Res(f, g) if deg g + deg p ≤ deg f.

theorem Polynomial.resultant_C_mul_right {R : Type u_1} [CommRing R] (f g : Polynomial R) (m n : ℕ) (r : R) : f.resultant (C r * g) m n = r ^ m * f.resultant g m n

Res(f, a • g) = a ^ {deg f} * Res(f, g).

theorem Polynomial.resultant_C_mul_left {R : Type u_1} [CommRing R] (f g : Polynomial R) (m n : ℕ) (r : R) : (C r * f).resultant g m n = r ^ n * f.resultant g m n

Res(a • f, g) = a ^ {deg g} * Res(f, g).

theorem Polynomial.resultant_succ_left_deg {R : Type u_1} [CommRing R] (f g : Polynomial R) (m n : ℕ) (hf : f.natDegree ≤ m) : f.resultant g (m + 1) n = (-1) ^ n * g.coeff n * f.resultant g m n

theorem Polynomial.resultant_add_left_deg {R : Type u_1} [CommRing R] (f g : Polynomial R) (m n k : ℕ) (hf : f.natDegree ≤ m) : f.resultant g (m + k) n = (-1) ^ (n * k) * g.coeff n ^ k * f.resultant g m n

theorem Polynomial.resultant_add_right_deg {R : Type u_1} [CommRing R] (f g : Polynomial R) (m n k : ℕ) (hg : g.natDegree ≤ n) : f.resultant g m (n + k) = f.coeff m ^ k * f.resultant g m n

theorem Polynomial.resultant_eq_zero_of_lt_lt {R : Type u_1} [CommRing R] (f g : Polynomial R) (m n : ℕ) (hf : f.natDegree < m) (hg : g.natDegree < n) : f.resultant g m n = 0

@[simp]

theorem Polynomial.resultant_C_left {R : Type u_1} [CommRing R] (g : Polynomial R) (m n : ℕ) (r : R) : (C r).resultant g m n = (-1) ^ (m * n) * g.coeff n ^ m * r ^ n

@[simp]

theorem Polynomial.resultant_C_right {R : Type u_1} [CommRing R] (f : Polynomial R) (m n : ℕ) (r : R) : f.resultant (C r) m n = f.coeff m ^ n * r ^ m

@[simp]

theorem Polynomial.resultant_one_left {R : Type u_1} [CommRing R] (g : Polynomial R) (m n : ℕ) : resultant 1 g m n = (-1) ^ (m * n) * g.coeff n ^ m

@[simp]

theorem Polynomial.resultant_one_right {R : Type u_1} [CommRing R] (f : Polynomial R) (m n : ℕ) : f.resultant 1 m n = f.coeff m ^ n

theorem Polynomial.resultant_X_sub_C_left {R : Type u_1} [CommRing R] (g : Polynomial R) (n : ℕ) (r : R) (hg : g.natDegree ≤ n) : (X - C r).resultant g 1 n = eval r g

Res(X - r, g) = g(r)

theorem Polynomial.resultant_X_sub_C_right {R : Type u_1} [CommRing R] (f : Polynomial R) (m : ℕ) (r : R) (hf : f.natDegree ≤ m) : f.resultant (X - C r) m 1 = (-1) ^ m * eval r f

Res(f, X - r) = (-1)^{deg f} * f(r)

noncomputable def Polynomial.discr {R : Type u_1} [CommRing R] (f : Polynomial R) : R

The discriminant of a polynomial, defined as the determinant of f.sylvesterDeriv modified by a sign. The sign is chosen so polynomials over ℝ with all roots real have non-negative discriminant.

Equations

• f.discr = f.sylvesterDeriv.det * (-1) ^ (f.natDegree * (f.natDegree - 1) / 2)

@[deprecated Polynomial.discr (since := "2025-10-20")]

def Polynomial.disc {R : Type u_1} [CommRing R] (f : Polynomial R) : R

Alias of Polynomial.discr.

---

The discriminant of a polynomial, defined as the determinant of f.sylvesterDeriv modified by a sign. The sign is chosen so polynomials over ℝ with all roots real have non-negative discriminant.

Equations

• @Polynomial.disc = @Polynomial.discr

@[simp]

theorem Polynomial.discr_C {R : Type u_1} [CommRing R] (r : R) : (C r).discr = 1

The discriminant of a constant polynomial is 1.

theorem Polynomial.discr_of_degree_eq_one {R : Type u_1} [CommRing R] {f : Polynomial R} (hf : f.degree = 1) : f.discr = 1

The discriminant of a linear polynomial is 1.

theorem Polynomial.discr_of_degree_eq_two {R : Type u_1} [CommRing R] {f : Polynomial R} (hf : f.degree = 2) : f.discr = f.coeff 1 ^ 2 - 4 * f.coeff 0 * f.coeff 2

Standard formula for the discriminant of a quadratic polynomial.

@[deprecated Polynomial.discr_C (since := "2025-10-20")]

theorem Polynomial.disc_C {R : Type u_1} [CommRing R] (r : R) : (C r).discr = 1

Alias of Polynomial.discr_C.

---

The discriminant of a constant polynomial is 1.

@[deprecated Polynomial.discr_of_degree_eq_one (since := "2025-10-20")]

theorem Polynomial.disc_of_degree_eq_one {R : Type u_1} [CommRing R] {f : Polynomial R} (hf : f.degree = 1) : f.discr = 1

Alias of Polynomial.discr_of_degree_eq_one.

---

The discriminant of a linear polynomial is 1.

@[deprecated Polynomial.discr_of_degree_eq_two (since := "2025-10-20")]

theorem Polynomial.disc_of_degree_eq_two {R : Type u_1} [CommRing R] {f : Polynomial R} (hf : f.degree = 2) : f.discr = f.coeff 1 ^ 2 - 4 * f.coeff 0 * f.coeff 2

Alias of Polynomial.discr_of_degree_eq_two.

---

Standard formula for the discriminant of a quadratic polynomial.

theorem Polynomial.resultant_deriv {R : Type u_1} [CommRing R] {f : Polynomial R} (hf : 0 < f.degree) : f.resultant (derivative f) f.natDegree (f.natDegree - 1) = (-1) ^ (f.natDegree * (f.natDegree - 1) / 2) * f.leadingCoeff * f.discr

Relation between the resultant and the discriminant.

(Note this is actually false when f is a constant polynomial not equal to 1, so the assumption on the degree is genuinely needed.)

theorem Polynomial.discr_of_degree_eq_three {R : Type u_1} [CommRing R] {f : Polynomial R} (hf : f.degree = 3) : f.discr = f.coeff 2 ^ 2 * f.coeff 1 ^ 2 - 4 * f.coeff 3 * f.coeff 1 ^ 3 - 4 * f.coeff 2 ^ 3 * f.coeff 0 - 27 * f.coeff 3 ^ 2 * f.coeff 0 ^ 2 + 18 * f.coeff 3 * f.coeff 2 * f.coeff 1 * f.coeff 0

Standard formula for the discriminant of a cubic polynomial.

@[deprecated Polynomial.discr_of_degree_eq_three (since := "2025-10-20")]

theorem Polynomial.disc_of_degree_eq_three {R : Type u_1} [CommRing R] {f : Polynomial R} (hf : f.degree = 3) : f.discr = f.coeff 2 ^ 2 * f.coeff 1 ^ 2 - 4 * f.coeff 3 * f.coeff 1 ^ 3 - 4 * f.coeff 2 ^ 3 * f.coeff 0 - 27 * f.coeff 3 ^ 2 * f.coeff 0 ^ 2 + 18 * f.coeff 3 * f.coeff 2 * f.coeff 1 * f.coeff 0

Alias of Polynomial.discr_of_degree_eq_three.

---

Standard formula for the discriminant of a cubic polynomial.