Theorems · Theorem · commutative algebra

Polynomial.resultant_deriv

∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R},
  0 < f.degree →
    f.resultant (Polynomial.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.)

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