dvd_iff_isRoot — Mathlib

English

A polynomial p ∈ R[X] is divisible by X − a if and only if a is a root of p.

Русский

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

LaTeX

$$$ X - a \mid p \iff p(a) = 0 $$$

Lean4

theorem dvd_iff_isRoot : X - C a ∣ p ↔ IsRoot p a :=
  ⟨fun h => by rwa [← modByMonic_eq_zero_iff_dvd (monic_X_sub_C _), modByMonic_X_sub_C_eq_C_eval, ← C_0, C_inj] at h,
    fun h => ⟨p /ₘ (X - C a), by rw [mul_divByMonic_eq_iff_isRoot.2 h]⟩⟩

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