English
The standard Sylvester matrix of f and f' is recovered from SylvesterDeriv by updating a specific row with a scaling by the leading coefficient.
Русский
Стандартная матрица Сильвестра f и f' восстанавливается из SylvesterDeriv обновлением определенной строки с масштабированием на главный коэффициент.
LaTeX
$$$(f\\,\\text{SylvesterDeriv}).\\text{updateRow}(\\langle 2 f^{\\,\\mathrm{natDegree}}-2, \\cdots \\rangle)\\big( f.leadingCoeff \\cdot (\\text{SylvesterDeriv}(f))\\big) = \\text{Sylvester}(f,f'.\\mathrm{natDegree},f'.\\mathrm{natDegree}-1)$$$
Lean4
/-- 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`. -/
theorem sylvesterDeriv_updateRow (f : R[X]) (hf : 0 < f.natDegree) :
(sylvesterDeriv f).updateRow ⟨2 * f.natDegree - 2, by cutsat⟩
(f.leadingCoeff • (sylvesterDeriv f ⟨2 * f.natDegree - 2, by cutsat⟩)) =
(sylvester f f.derivative f.natDegree (f.natDegree - 1)) :=
by
by_cases hn : f.natDegree = 0
· ext ⟨i, hi⟩; cutsat
ext ⟨i, hi⟩ ⟨j, hj⟩
rw [sylvesterDeriv, dif_neg hn]
rcases ne_or_eq i (2 * f.natDegree - 2) with hi' | rfl
· -- Top part of matrix
rw [Matrix.updateRow_ne (Fin.ne_of_val_ne hi'), Matrix.updateRow_ne (Fin.ne_of_val_ne hi')]
· -- Bottom row
simp only [sylvester, Fin.addCases, mem_Icc, coeff_derivative, eq_rec_constant, leadingCoeff, Matrix.updateRow_self,
Matrix.updateRow_apply, ↓reduceIte, Pi.smul_apply, smul_eq_mul, mul_ite, mul_one, mul_zero, Matrix.of_apply,
Fin.castLT_mk, tsub_le_iff_right, Fin.cast_mk, Fin.subNat_mk, dite_eq_ite]
split_ifs
on_goal 2 => rw [show f.natDegree = 1 by cutsat]
on_goal 3 =>
rw [← Nat.cast_one (R := R), ← Nat.cast_add, show f.natDegree = 1 by cutsat]
norm_num
on_goal 6 =>
rw [← Nat.cast_one (R := R), ← Nat.cast_add]
#adaptation_note /-- Prior to nightly-2025-09-09,
these two steps were not needed (i.e. `grind` just finished from here)
-/
have : 2 * f.natDegree - 2 - (j - (f.natDegree - 1)) + 1 = f.natDegree := by grind
simp [this]
all_goals grind
