English
If a monic polynomial p ∈ F[X] splits via f: F → F, and all roots of map f p have norm ≤ B with B < 0, then p = 1.
Русский
Если моноичный многочлен p ∈ F[X] раскладывается через f: F → F, и все корни map f p имеют норму ≤ B, причём B < 0, то p равно единице.
LaTeX
$$$B < 0 \\;\\land\\; p \\text{ моноичен} \\land\\; p \\text{ splits } f p \\land\\; (\\forall z \\in (map f p).\\text{roots}, \\|z\\| \\le B) \\Rightarrow p = 1$$$
Lean4
theorem eq_one_of_roots_le {p : F[X]} {f : F →+* K} {B : ℝ} (hB : B < 0) (h1 : p.Monic) (h2 : Splits f p)
(h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B) : p = 1 :=
h1.natDegree_eq_zero_iff_eq_one.mp
(by
contrapose! hB
rw [← h1.natDegree_map f, natDegree_eq_card_roots' h2] at hB
obtain ⟨z, hz⟩ := card_pos_iff_exists_mem.mp (zero_lt_iff.mpr hB)
exact le_trans (norm_nonneg _) (h3 z hz))
