dvd_comp_C_mul_X_add_C_iff — Mathlib

English

For polynomials p and q over a commutative ring, and for an invertible a and any b, p divides q composed with (C a · X + C b) if and only if p composed with (C a^{-1} · (X − C b)) divides q.

Русский

Для полиномов p и q над коммутативным кольцом и для обращаемого элемента a с b: p делит q ∘ (C a X + C b) тогда и только тогда, когда p ∘ (C a^{-1} (X − C b)) делит q.

LaTeX

$$$ p \mid q \circ (C a \cdot X + C b) \iff p \circ (C a^{-1} \cdot (X - C b)) \mid q $$$

Lean4

theorem dvd_comp_C_mul_X_add_C_iff (p q : R[X]) (a b : R) [Invertible a] :
    p ∣ q.comp (C a * X + C b) ↔ p.comp (C ⅟a * (X - C b)) ∣ q :=
  by
  convert map_dvd_iff <| algEquivCMulXAddC a b using 2
  simp [← comp_eq_aeval, comp_assoc, ← mul_assoc, ← C_mul]

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