dvd_iff_roots_le_roots — Mathlib

English

For p,q ∈ K[X], with p,Splits id, p ≠ 0, q ≠ 0, p ∣ q iff p.roots ≤ q.roots.

Русский

Для p,q ∈ K[X], с p распадается над id_K, p ≠ 0, q ≠ 0, верно: p делит q тогда и только тогда, когда p.roots ≤ q.roots.

LaTeX

$$$\\forall p,q:\\ Polynomial K,\\; (p.Splits(\\mathrm{id}_K)) \\land p \\neq 0 \\land q \\neq 0 \\Rightarrow (p \\mid q) \\iff (p.\\text{roots} \\le q.\\text{roots}).$$$

Lean4

theorem dvd_iff_roots_le_roots {p q : K[X]} (hp : p.Splits (RingHom.id _)) (hp0 : p ≠ 0) (hq0 : q ≠ 0) :
    p ∣ q ↔ p.roots ≤ q.roots :=
  ⟨Polynomial.roots.le_of_dvd hq0, hp.dvd_of_roots_le_roots hp0⟩

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