roots_eq_zero_iff — Mathlib

English

For a separable p ∈ k[X], p.roots = 0 if and only if p = C(p.coeff 0).

Русский

Для сепарабельного p ∈ k[X], множество корней p равно нулю тогда и только тогда, когда p = C(p.coeff 0).

LaTeX

$$p.Separable → p.roots = 0 ↔ p = Polynomial.C (p.coeff 0)$$

Lean4

theorem roots_eq_zero_iff [IsSepClosed k] {p : k[X]} (hsep : p.Separable) :
    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⟩ := IsSepClosed.exists_root p hd.ne' hsep
    rw [← mem_roots (ne_zero_of_degree_gt hd), h] at hz
    simp at hz

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