English
For a quadratic polynomial f, the discriminant equals f.coeff 1^2 − 4 f.coeff 0 f.coeff 2.
Русский
Для квадратичного полинома f дискриминант равен f.coeff 1^2 − 4 f.coeff 0 f.coeff 2.
LaTeX
$$$\\operatorname{disc} f = f.coeff 1^{2} - 4 \\cdot f.coeff 0 \\cdot f.coeff 2$$$
Lean4
/-- Standard formula for the discriminant of a quadratic polynomial. -/
theorem disc_of_degree_eq_two {f : R[X]} (hf : f.degree = 2) : disc f = f.coeff 1 ^ 2 - 4 * f.coeff 0 * f.coeff 2 :=
by
rw [← Nat.cast_two, degree_eq_iff_natDegree_eq_of_pos two_pos] at hf
let e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 3 := finCongr (by cutsat)
rw [disc, ← Matrix.det_reindex_self e]
have : f.sylvesterDeriv.reindex e e = !![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] :=
by
ext i j
fin_cases i <;> fin_cases j <;>
simp [e, sylvesterDeriv, sylvester, coeff_derivative, mul_comm, Fin.addCases, one_add_one_eq_two, hf, Fin.cast]
simp only [this, Matrix.det_fin_three, Matrix.of_apply, Matrix.cons_val', Matrix.cons_val_zero,
Matrix.cons_val_fin_one, Matrix.cons_val_one, Matrix.cons_val, hf]
ring_nf
