coeff_expand_mul — Mathlib

English

For p > 0, the coefficient at index n·p of the expanded polynomial equals the coefficient at index n of the original polynomial.

Русский

При p > 0 коэффициент при n·p в расщеплённом полиномe равен коэффициенту при n в исходном полиномe.

LaTeX

$$$(\operatorname{expand} R p f).\mathrm{coeff}(n \cdot p) = f.\mathrm{coeff}(n)$$$

Lean4

@[simp]
theorem coeff_expand_mul {p : ℕ} (hp : 0 < p) (f : R[X]) (n : ℕ) : (expand R p f).coeff (n * p) = f.coeff n := by
  rw [coeff_expand hp, if_pos (dvd_mul_left _ _), Nat.mul_div_cancel _ hp]

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