mul_divByMonic_eq_iff_isRoot — Mathlib

English

Let R be a commutative ring and p ∈ R[X], a ∈ R. Then p is divisible by X − a in R[X] if and only if a is a root of p.

Русский

Пусть R — коммутативное кольцо и p ∈ R[X], a ∈ R. Тогда p делится на X − a в R[X] тогда и только тогда, когда a является корнем p.

LaTeX

$$$ (X - a) \mid p \;\Longleftrightarrow\; p(a) = 0 $$$

Lean4

theorem mul_divByMonic_eq_iff_isRoot : (X - C a) * (p /ₘ (X - C a)) = p ↔ IsRoot p a :=
  .trans
    ⟨fun h => by rw [← h, eval_mul, eval_sub, eval_X, eval_C, sub_self, zero_mul], fun h => by
      conv_rhs =>
        rw [← modByMonic_add_div p (monic_X_sub_C a)]
        rw [modByMonic_X_sub_C_eq_C_eval, h, C_0, zero_add]⟩
    IsRoot.def.symm

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