disc_eq_prod_three_roots — Mathlib

English

Under a ≠ 0 and three roots x,y,z, the discriminant equals a^4 ∏_{i<j} (r_i − r_j)^2, i.e., (a^2 (x−y)(x−z)(y−z))^2.

Русский

При a ≠ 0 и трех корнях x,y,z дискриминант равен a^4 ∏_{i<j} (r_i − r_j)^2, то есть (a^2 (x−y)(x−z)(y−z))^2.

LaTeX

$$$$\\varphi P.disc = (\\varphi P.a \\cdot \\varphi P.a \\cdot (x - y) \\cdot (x - z) \\cdot (y - z))^2.$$$$

Lean4

theorem disc_eq_prod_three_roots (ha : P.a ≠ 0) (h3 : (map φ P).roots = { x, y, z }) :
    φ P.disc = (φ P.a * φ P.a * (x - y) * (x - z) * (y - z)) ^ 2 :=
  by
  simp only [disc, RingHom.map_add, RingHom.map_sub, RingHom.map_mul, map_pow, map_ofNat]
  rw [b_eq_three_roots ha h3, c_eq_three_roots ha h3, d_eq_three_roots ha h3]
  ring1

Похожие утверждения