Theorems · Theorem · commutative algebra

Polynomial.discr_of_degree_eq_three

∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R},
  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.

Defined in

Mathlib.RingTheory.Polynomial.Resultant.Basic

Cited by

0 results in Mathlib

Foundations

Depth 109 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRing