disc_ne_zero_iff_roots_nodup — Mathlib

English

Let a ≠ 0 and the mapped roots be x, y, z. Then disc ≠ 0 if and only if the roots are nodup (x, y, z are pairwise distinct).

Русский

Пусть a ≠ 0 и корни x, y, z. Тогда дискриминант ≠ 0 тогда и только тогда, когда корни узловые (x, y, z попарно различны).

LaTeX

$$$$\\operatorname{disc}(P) \\ne 0 \\iff (map\\varphi P).roots\\;\\text{Nodup}.$$$$

Lean4

theorem disc_ne_zero_iff_roots_nodup (ha : P.a ≠ 0) (h3 : (map φ P).roots = { x, y, z }) :
    P.disc ≠ 0 ↔ (map φ P).roots.Nodup :=
  by
  rw [disc_ne_zero_iff_roots_ne ha h3, h3]
  change _ ↔ (x ::ₘ y ::ₘ { z }).Nodup
  rw [nodup_cons, nodup_cons, mem_cons, mem_singleton, mem_singleton]
  simp only [nodup_singleton]
  tauto

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