ofPowerSeries_X_pow — Mathlib

English

For each natural number n, the Hahn series corresponding to X^n is the delta at exponent n with coefficient 1; i.e., coefficient 1 at n and 0 elsewhere.

Русский

Для каждого натурального числа n соответствующий X^n ряд Хана имеет вид дельты по экспоненте n: коэффициент при n равен 1, а при остальных экспонентах — 0.

LaTeX

$$$\\operatorname{coeff}_{\\gamma}\\big(\\operatorname{ofPowerSeries}_{\\Gamma,R}(\\mathrm{X}^{n})\\big)=\\begin{cases}1,&\\gamma=n\\\\0,&\\gamma\\neq n\\end{cases}$$$

Lean4

theorem ofPowerSeries_X_pow {R} [Semiring R] (n : ℕ) : ofPowerSeries Γ R (PowerSeries.X ^ n) = single (n : Γ) 1 := by
  simp
    -- Lemmas about converting hahn_series over fintype to and from mv_power_series

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