dvd_comp_X_add_C_iff — Mathlib

English

For polynomials p, q and a ∈ R, p divides q ∘ (X + C a) if and only if p ∘ (X − C a) divides q.

Русский

Для полиномов p, q и a ∈ R: p делит q ∘ (X + C a) тогда и только тогда, когда p ∘ (X − C a) делит q.

LaTeX

$$$ p \mid q \circ (X + C a) \iff p \circ (X - C a) \mid q $$$

Lean4

theorem dvd_comp_X_add_C_iff (p q : R[X]) (a : R) : p ∣ q.comp (X + C a) ↔ p.comp (X - C a) ∣ q := by
  simpa using dvd_comp_X_sub_C_iff p q (-a)

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