comp_C_mul_X_coeff — Mathlib

English

For any p ∈ R[X], r ∈ R and n ∈ ℕ, the coefficient at degree n of p ∘ (C r · X) equals p.coeff n · r^n.

Русский

Для любого p ∈ R[X], r ∈ R и n ∈ ℕ, коэффициент при степени n в p ∘ (C r · X) равен p.coeff n · r^n.

LaTeX

$$$(p.comp \\lvert C r * X \\rvert).coeff n = p.coeff n * r^n$$

Lean4

@[simp]
theorem comp_C_mul_X_coeff {r : R} {n : ℕ} : (p.comp <| C r * X).coeff n = p.coeff n * r ^ n :=
  by
  simp_rw [comp, eval₂_eq_sum_range, (commute_X _).symm.mul_pow, ← C_pow, finset_sum_coeff, coeff_C_mul, coeff_X_pow]
  rw [Finset.sum_eq_single n _ fun h ↦ ?_, if_pos rfl, mul_one]
  · intro b _ h; simp_rw [if_neg h.symm, mul_zero]
  · rw [coeff_eq_zero_of_natDegree_lt, zero_mul]
    rwa [Finset.mem_range_succ_iff, not_le] at h

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