disc_ne_zero_iff_roots_ne — Mathlib

English

If a ≠ 0 and the mapped roots are x, y, z, then disc ≠ 0 iff the roots are pairwise distinct: x ≠ y ∧ x ≠ z ∧ y ≠ z.

Русский

Если a ≠ 0 и корни равны x, y, z, то дискриминант ≠ 0 тогда и только тогда, когда корни попарно различны: x ≠ y ∧ x ≠ z ∧ y ≠ z.

LaTeX

$$$$\\operatorname{disc}(P) \\ne 0 \\iff x \\ne y \\land x \\ne z \\land y \\ne z.$$$$

Lean4

theorem disc_ne_zero_iff_roots_ne (ha : P.a ≠ 0) (h3 : (map φ P).roots = { x, y, z }) :
    P.disc ≠ 0 ↔ x ≠ y ∧ x ≠ z ∧ y ≠ z :=
  by
  rw [← _root_.map_ne_zero φ, disc_eq_prod_three_roots ha h3, pow_two]
  simp_rw [mul_ne_zero_iff, sub_ne_zero, _root_.map_ne_zero, and_self_iff, and_iff_right ha, and_assoc]

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