Theorems · Theorem · commutative algebra

Polynomial.sylvesterDeriv_updateRow

∀ {R : Type u_1} [inst : Semiring R] (f : Polynomial R) (hf : 0 < f.natDegree),
  f.sylvesterDeriv.updateRow ⟨2 * f.natDegree - 2, ⋯⟩ (f.leadingCoeff • f.sylvesterDeriv ⟨2 * f.natDegree - 2, ⋯⟩) =
    (Polynomial.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.

Defined in

Mathlib.RingTheory.Polynomial.Resultant.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

Semiring