dvd_term_of_isRoot_of_dvd_terms — Mathlib

English

If hr: f.IsRoot r and h: ∀ j ≠ i, p ∣ f.coeff j · r^j, then p ∣ f.coeff i · r^i.

Русский

Если hr: f IsRoot r и h: ∀ j ≠ i, p ∣ f.coeff j · r^j, то p ∣ f.coeff i · r^i.

LaTeX

$$f.IsRoot r → (∀ j ≠ i, p ∣ f.coeff j · r^j) → p ∣ f.coeff i · r^i$$

Lean4

theorem dvd_term_of_isRoot_of_dvd_terms {r p : S} {f : S[X]} (i : ℕ) (hr : f.IsRoot r)
    (h : ∀ j ≠ i, p ∣ f.coeff j * r ^ j) : p ∣ f.coeff i * r ^ i :=
  dvd_term_of_dvd_eval_of_dvd_terms i (Eq.symm hr ▸ dvd_zero p) h

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