English
As before, left multiplication by C(r) equals r times the series.
Русский
Как и прежде, левое умножение на C(r) равно умножению на скаляр r.
LaTeX
$$$ C(r) \cdot x = r \cdot x $$$
Lean4
/-- The ring `HahnSeries ℕ R` is isomorphic to `PowerSeries R`. -/
@[simps]
def toPowerSeries : HahnSeries ℕ R ≃+* PowerSeries R
where
toFun f := PowerSeries.mk f.coeff
invFun f := ⟨fun n => PowerSeries.coeff n f, .of_linearOrder _⟩
left_inv
f := by
ext
simp
right_inv
f := by
ext
simp
map_add' f
g := by
ext
simp
map_mul' f
g := by
ext n
simp only [PowerSeries.coeff_mul, PowerSeries.coeff_mk, coeff_mul]
classical
refine (sum_filter_ne_zero _).symm.trans <| (sum_congr ?_ fun _ _ ↦ rfl).trans <| sum_filter_ne_zero _
ext m
simp only [mem_antidiagonal, mem_addAntidiagonal, and_congr_left_iff, mem_filter, mem_support]
rintro h
rw [and_iff_right (left_ne_zero_of_mul h), and_iff_right (right_ne_zero_of_mul h)]
