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

@[simp]

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)

@[simp]

theorem Polynomial.resultant_X_add_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)

@[simp]

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)

@[simp]

theorem Polynomial.resultant_X_add_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)

theorem Polynomial.resultant_eq_prod_roots_sub {K : Type u_3} [Field K] (f g : Polynomial K) (hf : f.Monic) (hg : g.Monic) (hf' : f.Splits) (hg' : g.Splits) : f.resultant g = (Multiset.map (fun (ij : K × K) => ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod

If f and g are monic and splits, then Res(f, g) = ∏ (α - β), where α and β runs through the roots of f and g respectively.

theorem Polynomial.resultant_eq_prod_eval {R : Type u_1} [CommRing R] [IsDomain R] (f g : Polynomial R) (n : ℕ) (hg : g.natDegree ≤ n) (hf : f.Splits) : f.resultant g f.natDegree n = f.leadingCoeff ^ n * (Multiset.map (fun (x : R) => eval x g) f.roots).prod

If f splits with leading coeff a and degree n, then Res(f, g) = aⁿ * ∏ g(α) where α runs through the roots of f.

theorem Polynomial.induction_of_Splits_of_injective_of_surjective {R : Type u} [CommRing R] (p : Polynomial R) (P : {R : Type u} → [inst : CommRing R] → Polynomial R → Prop) (Splits : ∀ (R : Type u) [inst : Field R] (p : Polynomial R), p.Splits → P p) (injective : ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S), Function.Injective ⇑φ → ∀ (p : Polynomial R), P (map φ p) → P p) (surjective : ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S), Function.Surjective ⇑φ → ∀ (p : Polynomial S), (∀ (q : Polynomial R), P q) → P p) : P p

An induction principle useful to prove statements about resultants. Let P be a predicate on a polynomial. If R → S injective implies (∀ p : S[X], P p) → (∀ p : R[X], P p), and if R → S surjective implies (∀ p : R[X], P p) → (∀ p : S[X], P p), then we may reduce to the case where R is a field and p splits.

theorem Polynomial.resultant_mul_right {R : Type u_1} [CommRing R] (f g₁ g₂ : Polynomial R) (m : ℕ) (hm : f.natDegree ≤ m) : f.resultant (g₁ * g₂) m (g₁.natDegree + g₂.natDegree) = f.resultant g₁ m * f.resultant g₂ m

Res(f, g₁ * g₂) = Res(f, g₁) * Res(f, g₂).

theorem Polynomial.resultant_mul_left {R : Type u_1} [CommRing R] (f₁ f₂ g : Polynomial R) (n : ℕ) (hn : g.natDegree ≤ n) : (f₁ * f₂).resultant g (f₁.natDegree + f₂.natDegree) n = f₁.resultant g f₁.natDegree n * f₂.resultant g f₂.natDegree n

Res(f₁ * f₂, g) = Res(f₁, g) * Res(f₂, g).

@[simp]

theorem Polynomial.resultant_self {R : Type u_1} [CommRing R] (f : Polynomial R) : f.resultant f = 0 ^ f.natDegree

Res(f, f) = 0 unless deg f = 0. Also see resultant_self_eq_zero.

theorem Polynomial.resultant_self_eq_zero {R : Type u_1} [CommRing R] (f : Polynomial R) (h : f.natDegree ≠ 0) : f.resultant f = 0

theorem Polynomial.resultant_dvd_leadingCoeff_pow {R : Type u_1} [CommRing R] [IsDomain R] (f g : Polynomial R) (H : IsCoprime f g) : ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n

theorem Polynomial.resultant_ne_zero {R : Type u_1} [CommRing R] [IsDomain R] (f g : Polynomial R) (H : IsCoprime f g) : f.resultant g ≠ 0

@[simp]

theorem Polynomial.resultant_prod_left {R : Type u_1} [CommRing R] {ι : Type u_3} (s : Finset ι) (f : ι → Polynomial R) (g : Polynomial R) (n : ℕ) (hf : ∏ i ∈ s, (f i).leadingCoeff ≠ 0) (hn : g.natDegree ≤ n) : (∏ i ∈ s, f i).resultant g (∏ i ∈ s, f i).natDegree n = ∏ i ∈ s, (f i).resultant g (f i).natDegree n

@[simp]

theorem Polynomial.resultant_prod_right {R : Type u_1} [CommRing R] {ι : Type u_3} (s : Finset ι) (f : Polynomial R) (g : ι → Polynomial R) (m : ℕ) (hm : f.natDegree ≤ m) (hg : ∏ i ∈ s, (g i).leadingCoeff ≠ 0) : f.resultant (∏ i ∈ s, g i) m = ∏ i ∈ s, f.resultant (g i) m

@[simp]

theorem Polynomial.resultant_pow_left {R : Type u_1} [CommRing R] (f g : Polynomial R) (m n : ℕ) (hf : f.leadingCoeff ^ m ≠ 0) (hn : g.natDegree ≤ n) : (f ^ m).resultant g (f ^ m).natDegree n = f.resultant g f.natDegree n ^ m

@[simp]

theorem Polynomial.resultant_pow_right {R : Type u_1} [CommRing R] (f g : Polynomial R) (m n : ℕ) (hm : f.natDegree ≤ m) (hg : g.leadingCoeff ^ n ≠ 0) : f.resultant (g ^ n) m = f.resultant g m ^ n

theorem Polynomial.resultant_X_sub_C_pow_left {R : Type u_1} [CommRing R] (r : R) (g : Polynomial R) (m n : ℕ) (hn : g.natDegree ≤ n) : ((X - C r) ^ m).resultant g m n = eval r g ^ m

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

theorem Polynomial.resultant_X_pow_left {R : Type u_1} [CommRing R] (g : Polynomial R) (m n : ℕ) (hn : g.natDegree ≤ n) : (X ^ m).resultant g m n = g.coeff 0 ^ m

theorem Polynomial.resultant_X_pow_right {R : Type u_1} [CommRing R] (f : Polynomial R) (m n : ℕ) (hm : f.natDegree ≤ m) : f.resultant (X ^ n) m n = (-1) ^ (m * n) * f.coeff 0 ^ n

theorem Polynomial.resultant_scaleRoots {R : Type u_1} [CommRing R] (f g : Polynomial R) (r : R) : (f.scaleRoots r).resultant (g.scaleRoots r) = r ^ (f.natDegree * g.natDegree) * f.resultant g

theorem Polynomial.resultant_integralNormalization {R : Type u_1} [CommRing R] (f g : Polynomial R) (hg : g.natDegree ≠ 0) : (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization = g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g

theorem Polynomial.resultant_taylor {R : Type u_1} [CommRing R] (f g : Polynomial R) (r : R) : ((taylor r) f).resultant ((taylor r) g) = f.resultant g

Res(f(x + r), g(x + r)) = Res(f, g).

noncomputable def Polynomial.sylvesterMap {m n : ℕ} {R : Type u_1} [CommRing R] (f g : Polynomial R) (hf : f.natDegree ≤ m) (hg : g.natDegree ≤ n) : ↥(degreeLT R m) × ↥(degreeLT R n) →ₗ[R] ↥(degreeLT R (m + n))

The map (p, q) ↦ f * q + g * p whose associated matrix is Syl(f, g).

Equations

• f.sylvesterMap g hf hg = { toFun := fun (pq : ↥(Polynomial.degreeLT R m) × ↥(Polynomial.degreeLT R n)) => ⟨f * ↑pq.2 + g * ↑pq.1, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Polynomial.sylvesterMap_apply_coe {m n : ℕ} {R : Type u_1} [CommRing R] (f g : Polynomial R) (hf : f.natDegree ≤ m) (hg : g.natDegree ≤ n) (pq : ↥(degreeLT R m) × ↥(degreeLT R n)) : ↑((f.sylvesterMap g hf hg) pq) = f * ↑pq.2 + g * ↑pq.1

theorem Polynomial.toMatrix_sylvesterMap {m n : ℕ} {R : Type u_1} [CommRing R] (f g : Polynomial R) (hf : f.natDegree ≤ m) (hg : g.natDegree ≤ n) : (LinearMap.toMatrix ((degreeLT.basis R m).prod (degreeLT.basis R n)) (degreeLT.basis R (m + n))) (f.sylvesterMap g hf hg) = (Matrix.reindex (Equiv.refl (Fin (m + n))) finSumFinEquiv.symm) (f.sylvester g m n)

theorem Polynomial.toMatrix_sylvesterMap' {m n : ℕ} {R : Type u_1} [CommRing R] (f g : Polynomial R) (hf : f.natDegree ≤ m) (hg : g.natDegree ≤ n) : (LinearMap.toMatrix (((degreeLT.basis R m).prod (degreeLT.basis R n)).reindex finSumFinEquiv) (degreeLT.basis R (m + n))) (f.sylvesterMap g hf hg) = f.sylvester g m n

noncomputable def Polynomial.adjSylvester {m n : ℕ} {R : Type u_1} [CommRing R] (f g : Polynomial R) : ↥(degreeLT R (m + n)) →ₗ[R] ↥(degreeLT R m) × ↥(degreeLT R n)

The adjugate map of the sylvester map. It takes P to (p, q) such that f * q + g * p = Res(f, g) * P.

Equations

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

theorem Polynomial.sylveserMap_comp_adjSylvester {m n : ℕ} {R : Type u_1} [CommRing R] (f g : Polynomial R) (hf : f.natDegree ≤ m) (hg : g.natDegree ≤ n) : f.sylvesterMap g hf hg ∘ₗ f.adjSylvester g = f.resultant g m n • LinearMap.id

theorem Polynomial.adjSylvester_comp_sylveserMap {m n : ℕ} {R : Type u_1} [CommRing R] (f g : Polynomial R) (hf : f.natDegree ≤ m) (hg : g.natDegree ≤ n) : f.adjSylvester g ∘ₗ f.sylvesterMap g hf hg = f.resultant g m n • LinearMap.id

theorem Polynomial.exists_mul_add_mul_eq_C_resultant {m n : ℕ} {R : Type u_1} [CommRing R] (f g : Polynomial R) (hf : f.natDegree ≤ m) (hg : g.natDegree ≤ n) (H : m ≠ 0 ∨ n ≠ 0) : ∃ (p : Polynomial R) (q : Polynomial R), p.degree < ↑n ∧ q.degree < ↑m ∧ f * p + g * q = C (f.resultant g m n)

Note that if n = m = 0 then resultant = 1 but f and g aren't necessarily coprime.

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.