Theorems · Definition · commutative algebra

Polynomial.sylvesterDeriv

{R : Type u_1} →
  [inst : 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.

Defined in

Mathlib.RingTheory.Polynomial.Resultant.Basic

Cited by

6 results in Mathlib

Foundations

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

Assumes

Semiring