coeff_expand_mul' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem coeff_expand_mul' {p : ℕ} (hp : 0 < p) (f : R[X]) (n : ℕ) : (expand R p f).coeff (p * n) = f.coeff n := by
  rw [mul_comm, coeff_expand_mul hp]

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