English
Relation between the resultant of f with its derivative and the discriminant: Res(f, f') equals ± leadingCoeff times the discriminant up to a sign depending on degree.
Русский
Связь результанта f и его производной f' с дискриминантом: Res(f,f') равен ± главному коэффициенту умноженному на дискриминант с учётом знака, зависящего от степени.
LaTeX
$$$\\operatorname{resultant}(f,f') = (-1)^{\\frac{f.natDegree( f.natDegree-1)}{2}} \\cdot f.leadingCoeff \\cdot f.disc$ (при некоторых условиях) $$
Lean4
/-- 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.) -/
theorem resultant_deriv {f : R[X]} (hf : 0 < f.degree) :
resultant f f.derivative f.natDegree (f.natDegree - 1) =
(-1) ^ (f.natDegree * (f.natDegree - 1) / 2) * f.leadingCoeff * f.disc :=
by
rw [← natDegree_pos_iff_degree_pos] at hf
rw [resultant, ← sylvesterDeriv_updateRow f hf, Matrix.det_updateRow_smul, Matrix.updateRow_eq_self, disc]
suffices ∀ (r s : R), s * r = s * r * (-1) ^ (f.natDegree * (f.natDegree - 1) / 2 * 2)
by
ring_nf
apply this
simp only [mul_comm _ 2, pow_mul, neg_one_sq, one_pow, mul_one, implies_true]
