coeff_coe — Mathlib

English

For any polynomial φ in MvPolynomial σ R and any coefficient index n, the coefficient of n in the embedded power series ↑φ equals the coefficient of n in φ.

Русский

Для любого многочлена φ ∈ MvPolynomial σ R и любого индекса коэффициента n коэффициент при n в вложенной степенной серии ↑φ совпадает с коэффициентом при n в φ.

LaTeX

$$$\\operatorname{coeff}_n(\\uparrow\\phi) = \\operatorname{coeff}_n \\phi$$$

Lean4

@[simp, norm_cast]
theorem coeff_coe (n : σ →₀ ℕ) : MvPowerSeries.coeff n ↑φ = coeff n φ :=
  rfl

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