English
For any f ∈ PowerSeries R and integer i, the i-th coefficient of the coerced f is 0 if i < 0, otherwise it equals PowerSeries.coeff |i| f.
Русский
Для любого степенного ряда f и целого i коэффициент i-ый от отображённого f равен 0, если i < 0; иначе — коэффициент степенного ряда при индексе |i|.
LaTeX
$$$\big( (f : R⟦X⟧) : R⸨X⸩ \big)_{i} = \begin{cases} 0, & i < 0 \\ PowerSeries.coeff (|i|) f, & i \ge 0 \end{cases}$$$
Lean4
theorem coeff_coe (i : ℤ) : ((f : R⟦X⟧) : R⸨X⸩).coeff i = if i < 0 then 0 else PowerSeries.coeff i.natAbs f :=
by
cases i
· rw [Int.ofNat_eq_coe, coeff_coe_powerSeries, if_neg (Int.natCast_nonneg _).not_gt, Int.natAbs_natCast]
· rw [ofPowerSeries_apply, embDomain_notin_image_support, if_pos (Int.negSucc_lt_zero _)]
simp only [not_exists, RelEmbedding.coe_mk, Set.mem_image, not_and, Function.Embedding.coeFn_mk, Ne,
toPowerSeries_symm_apply_coeff, mem_support, imp_true_iff, not_false_iff, reduceCtorEq]
