Polynomial where all roots are zero

Stream: Is there code for X?

[Edison Xie]

I know we have Polynomial.roots_X_pow which shows roots of X^n are zero and IsAlgClosed means every polynomial over it splits, but do we have that if the roots of a polynomial p : K[X] only has root zero where K is an algebraically closed field, then p is of the form a • X^n where a is not zero?

[Lawrence Wu (llllvvuu)]

Does docs#Polynomial.eq_prod_roots_of_splits_id plus docs#Polynomial.leadingCoeff_ne_zero plus docs#Polynomial.roots_zero work?

[Edison Xie]

docs#Polynomial.roots_zero is saying the roots of zero polynomial is zero, I'm not sure it's relevant here?

[Violeta Hernández]

The more general result is that a polynomial with only the root a is a scalar multiple of a power of X - a

[Violeta Hernández]

Which should be a trivial consequence of docs#Polynomial.eq_prod_roots_of_splits_id

[Edison Xie]

Thanks! I've got :

import Mathlib

lemma Polynomial.roots_zero_iff {K : Type*} [Field K] [IsAlgClosed K] {p : Polynomial K} :
    (∀ x ∈ p.roots, x = 0) ↔ ∃ a : K, p = a • Polynomial.X ^ p.natDegree :=
  ⟨fun hp ↦ by
  have hp' := Polynomial.eq_prod_roots_of_splits_id <| IsAlgClosed.splits p
  refine ⟨p.leadingCoeff, ?_⟩
  have : (Multiset.map (fun a ↦ X - C a) p.roots) = Multiset.replicate p.natDegree X :=
  Multiset.eq_replicate.2 ⟨by simpa using Polynomial.splits_iff_card_roots.1 <| IsAlgClosed.splits p,
    fun y hy ↦ by obtain ⟨z, hz1, hz2⟩ := Multiset.mem_map.1 hy; simpa [hp z hz1] using hz2.symm⟩
  simp only [this, Multiset.prod_replicate] at hp'
  nth_rw 1 [hp', smul_eq_C_mul], fun ⟨a, ha⟩ x ↦ by
  if ha' : a = 0 then simp_all +singlePass else
  rw [ha, Polynomial.smul_eq_C_mul, roots_C_mul_X_pow ha'] ; simp⟩

lemma Polynomial.roots_zero_iff' {K : Type*} [Field K] [IsAlgClosed K] {p : Polynomial K}
    (hp : p.Monic) : (∀ x ∈ p.roots, x = 0) ↔ p = X ^ p.natDegree :=
  propext (Polynomial.roots_zero_iff (p := p)) ▸ ⟨fun ⟨a, ha⟩ ↦ by
  nth_rw 1 [ha, smul_eq_C_mul]
  rw [← coeff_inj] at ha
  simp only [ne_eq, pow_eq_zero_iff', X_ne_zero, false_and, not_false_eq_true, mul_eq_right₀]
  have : p.leadingCoeff = _ := congr($ha p.natDegree)
  simp [hp] at this
  simp [this.symm], fun hp' ↦ ⟨1, by simp_all +singlePass⟩⟩

[Lawrence Wu (llllvvuu)]

docs#Polynomial.roots_zero is saying the roots of zero polynomial is zero, I'm not sure it's relevant here?

I included that for completeness to fulfill your condition that a is nonzero, but yes that part is probably automated