mul_X_sub_intCast_comp — Mathlib

English

For any polynomial p ∈ R[X], any r ∈ R and n ∈ ℕ, (p · (X − (n : R[X]))) .comp q = p.comp q · (q − n).

Русский

Для любого полинома p и натурального n: (p · (X − n)).comp q = p.comp q · (q − n).

LaTeX

$$$(p * (X - (n : R[X]))).comp\\ q = p.comp\\ q * (q - n)$$$

Lean4

theorem mul_X_sub_intCast_comp {n : ℕ} : (p * (X - (n : R[X]))).comp q = p.comp q * (q - n) := by
  rw [mul_sub, sub_comp, mul_X_comp, ← Nat.cast_comm, natCast_mul_comp, Nat.cast_comm, mul_sub]

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