X_sub_C_pow_dvd_iff — Mathlib

English

For a commutative ring R, p ∈ R[X], t ∈ R, and n ∈ ℕ, (X − C t)^n divides p if and only if X^n divides p ∘ (X + C t).

Русский

Для коммутативного кольца R, p ∈ R[X], t ∈ R и n ∈ ℕ верно: (X − C t)^n делит p тогда и только тогда, когда X^n делит p ∘ (X + C t).

LaTeX

$$$ (X - C t)^n \mid p \iff X^n \mid p\circ (X + C t) $$$

Lean4

theorem X_sub_C_pow_dvd_iff {n : ℕ} : (X - C t) ^ n ∣ p ↔ X ^ n ∣ p.comp (X + C t) :=
  by
  convert (map_dvd_iff <| algEquivAevalXAddC t).symm using 2
  simp [C_eq_algebraMap]

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