eval₂_modByMonic_eq_self_of_root

English

Let f : R →+* S and q ∈ R[X] be monic. If x ∈ S satisfies q.eval₂ f x = 0, then for any p ∈ R[X], (p modByMonic q).eval₂ f x = p.eval₂ f x.

Русский

Пусть f : R →+* S и q ∈ R[X] моноик. Если x ∈ S удовлетворяет q.eval₂ f x = 0, тогда для любого p ∈ R[X] выполняется (p modByMonic q).eval₂ f x = p.eval₂ f x.

LaTeX

$$$ \text{If } q \text{ is monic and } q(eval_2\ f\, x) = 0, \text{ then } (p \bmod q).eval_2\ f\ x = p.eval_2\ f\ x. $$$

Lean4

theorem eval₂_modByMonic_eq_self_of_root [CommRing S] {f : R →+* S} {p q : R[X]} (hq : q.Monic) {x : S}
    (hx : q.eval₂ f x = 0) : (p %ₘ q).eval₂ f x = p.eval₂ f x := by
  rw [modByMonic_eq_sub_mul_div p hq, eval₂_sub, eval₂_mul, hx, zero_mul, sub_zero]

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