X_sub_C_mul_divByMonic_eq_sub_modByMonic

English

For any ring K and f ∈ K[X], the identity (X − C a) · (f ÷ₘ (X − C a)) = f − f %ₘ (X − C a) holds, expressing the remainder upon division by the monic X − C a.

Русский

Для кольца K и полинома f в K[X] выполняется тождество (X − C a) · (f ÷ₘ (X − C a)) = f − f %ₘ (X − C a), выражающее остаток при делении на монику X − C a.

LaTeX

$$$ (X - C a) * (f /ₘ (X - C a)) = f - f %ₘ (X - C a)$$$

Lean4

theorem X_sub_C_mul_divByMonic_eq_sub_modByMonic {K : Type*} [Ring K] (f : K[X]) (a : K) :
    (X - C a) * (f /ₘ (X - C a)) = f - f %ₘ (X - C a) :=
  by
  rw [eq_sub_iff_add_eq, ← eq_sub_iff_add_eq', modByMonic_eq_sub_mul_div]
  exact monic_X_sub_C a

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