English
Let X denote the indeterminate in the power series and consider the Hahn series corresponding to it. Then the Hahn series has coefficient 1 at exponent 1 and coefficient 0 at all other exponents.
Русский
Пусть X обозначает неизвестное в степенном ряде, и рассмотрим соответствующий ему ряд Хана. Тогда коэффициент при экспоненте 1 равен 1, а при всех остальных экспонентах равен 0.
LaTeX
$$$\\operatorname{coeff}_{\\gamma}\\big(\\operatorname{ofPowerSeries}_{\\Gamma,R}(\\mathrm{X})\\big)=\\begin{cases}1,&\\gamma=1\\\\0,&\\gamma\\neq 1\\end{cases}$$$
Lean4
@[simp]
theorem ofPowerSeries_X : ofPowerSeries Γ R PowerSeries.X = single 1 1 :=
by
ext n
simp only [coeff_single, ofPowerSeries_apply]
split_ifs with hn
· rw [hn]
convert embDomain_coeff (a := 1) <;> simp
· rw [embDomain_notin_image_support]
simp only [not_exists, Set.mem_image, toPowerSeries_symm_apply_coeff, mem_support, PowerSeries.coeff_X]
intro
simp +contextual [Ne.symm hn]
