dvd_comp_neg_X_iff — Mathlib

English

For polynomials p, q with coefficients in a commutative ring, p divides q ∘ (−X) if and only if p ∘ (−X) divides q.

Русский

Пусть p, q — полиномы над коммутативным кольцом. Тогда p делит q ∘ (−X) тогда и только тогда, когда p ∘ (−X) делит q.

LaTeX

$$$ p \mid q \circ (-X) \iff p \circ (-X) \mid q $$$

Lean4

theorem dvd_comp_neg_X_iff (p q : R[X]) : p ∣ q.comp (-X) ↔ p.comp (-X) ∣ q :=
  by
  let _ := invertibleOne (α := R)
  let _ := invertibleNeg (R := R) 1
  simpa using dvd_comp_C_mul_X_add_C_iff p q (-1) 0

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