dvd_of_roots_le_roots — Mathlib

English

If p,Splits id, p ≠ 0, q has roots at least as many as p, then p divides q.

Русский

Если p распадается над идентичным отображением, p ≠ 0, а q имеет корни не менее чем p, то p делит q.

LaTeX

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

Lean4

theorem dvd_of_roots_le_roots {p q : K[X]} (hp : p.Splits (RingHom.id _)) (hp0 : p ≠ 0) (hq : p.roots ≤ q.roots) :
    p ∣ q := by
  rw [eq_prod_roots_of_splits_id hp, C_mul_dvd (leadingCoeff_ne_zero.2 hp0)]
  exact dvd_trans (Multiset.prod_dvd_prod_of_le (Multiset.map_le_map hq)) (prod_multiset_X_sub_C_dvd _)

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