ofPowerSeries_C — Mathlib

English

The image under ofPowerSeries of a PowerSeries constant C r equals HahnSeries constant C r.

Русский

Образ отображения ofPowerSeries при постоянной C r равен HahnSeries-константе C r.

LaTeX

$$$ ofPowerSeries\_Γ\ R (PowerSeries.C\ r) = HahnSeries.C\ r $$$

Lean4

@[simp]
theorem ofPowerSeries_C (r : R) : ofPowerSeries Γ R (PowerSeries.C r) = HahnSeries.C r :=
  by
  ext n
  simp only [ofPowerSeries_apply, C, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk, coeff_single]
  split_ifs with hn
  · subst hn
    convert embDomain_coeff (a := 0) <;> simp
  · rw [embDomain_notin_image_support]
    simp only [not_exists, Set.mem_image, toPowerSeries_symm_apply_coeff, mem_support, PowerSeries.coeff_C]
    intro
    simp +contextual [Ne.symm hn]

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