English
Definition: The Sylvester matrix for f and f'.derivative, modified by dividing the bottom row by the leading coefficient of f.
Русский
Определение: матрица Сильвестра для f и производной f', модифицированная делением нижней строки на главный коэффициент f.
LaTeX
$$$\\text{SylvesterDeriv}(f) = \\text{(modified Sylvester matrix of } f \\text{ and } f')$$$
Lean4
/-- 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`.
-/
noncomputable def sylvesterDeriv (f : R[X]) :
Matrix (Fin (f.natDegree - 1 + f.natDegree)) (Fin (f.natDegree - 1 + f.natDegree)) R :=
letI n := f.natDegree
if hn : n = 0 then 0
else
(f.sylvester f.derivative n (n - 1)).updateRow ⟨2 * n - 2, by cutsat⟩
(fun j ↦ if ↑j = n - 2 then 1 else (if ↑j = 2 * n - 2 then n else 0))
