roots_eq_zero_iff — Mathlib

English

Over an algebraically closed field, the roots of a polynomial p are precisely the elements a for which p(a)=0; equivalently, p.roots = 0 iff p is constant.

Русский

В алгебраически замкнутом поле корни многочлена совпадают с теми элементами, для которых p(a)=0; иначе p.roots = 0 тогда и только тогда, когда p константен.

LaTeX

$$$p.roots = 0 \iff p = C(p.coeff 0)$$$

Lean4

theorem roots_eq_zero_iff [IsAlgClosed k] {p : k[X]} : p.roots = 0 ↔ p = Polynomial.C (p.coeff 0) :=
  by
  refine ⟨fun h => ?_, fun hp => by rw [hp, roots_C]⟩
  rcases le_or_gt (degree p) 0 with hd | hd
  · exact eq_C_of_degree_le_zero hd
  · obtain ⟨z, hz⟩ := IsAlgClosed.exists_root p hd.ne'
    rw [← mem_roots (ne_zero_of_degree_gt hd), h] at hz
    simp at hz

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