dvd_comp_X_sub_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_sub_C_iff (p q : R[X]) (a : R) : p ∣ q.comp (X - C a) ↔ p.comp (X + C a) ∣ q :=
  by
  let _ := invertibleOne (α := R)
  simpa using dvd_comp_C_mul_X_add_C_iff p q 1 (-a)

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