English
For a cubic polynomial f, the discriminant equals a long explicit expression in the coefficients: coeff 2^2 coeff 1^2 − 4 coeff 3 coeff 1^3 − 4 coeff 2^3 coeff 0 − 27 coeff 3^2 coeff 0^2 + 18 coeff 3 coeff 2 coeff 1 coeff 0.
Русский
Для кубического полинома f дискриминант выражается через коэффициенты в виде длинного явного выражения: ...
LaTeX
$$$\\operatorname{disc}f = f.coeff 2^{2} f.coeff 1^{2} - 4 f.coeff 3 f.coeff 1^{3} - 4 f.coeff 2^{3} f.coeff 0 - 27 f.coeff 3^{2} f.coeff 0^{2} + 18 f.coeff 3 f.coeff 2 f.coeff 1 f.coeff 0$$$
Lean4
/-- Standard formula for the discriminant of a cubic polynomial. -/
theorem disc_of_degree_eq_three {f : R[X]} (hf : f.degree = 3) :
disc f =
f.coeff 2 ^ 2 * f.coeff 1 ^ 2 - 4 * f.coeff 3 * f.coeff 1 ^ 3 - 4 * f.coeff 2 ^ 3 * f.coeff 0 -
27 * f.coeff 3 ^ 2 * f.coeff 0 ^ 2 +
18 * f.coeff 3 * f.coeff 2 * f.coeff 1 * f.coeff 0 :=
by
apply natDegree_eq_of_degree_eq_some at hf
let e : Fin ((f.natDegree - 1) + f.natDegree) ≃ Fin 5 := finCongr (by rw [hf])
rw [disc, ← Matrix.det_reindex_self e, sylvesterDeriv_of_natDegree_eq_three hf]
simp [Matrix.det_succ_row_zero (n := 4), Matrix.det_succ_row_zero (n := 3), Fin.succAbove, Matrix.det_fin_three,
Finset.sum_fin_eq_sum_range, Finset.sum_range_succ, hf]
ring_nf
