ofFinsuppLinearMap — Mathlib

English

There is a linear map from (Γ →₀ V) to HahnSeries Γ V given by mapping a finitely supported function to the corresponding Hahn series; this map is R-linear.

Русский

Существует линейное отображение из (Γ →₀ V) в HahnSeries Γ V, которое отправляет конечноподдерживаемую функцию в соответствующий ряд Хана; это отображение линейно по R.

LaTeX

$$$\\text{ofFinsuppLinearMap} : (Γ \\to_0 V) \\to_{L[R]} HahnSeries(Γ,V)$$$

Lean4

/-- `ofFinsupp` as a linear map. -/
def ofFinsuppLinearMap : (Γ →₀ V) →ₗ[R] HahnSeries Γ V
    where
  toFun := ofFinsupp
  map_add' _
    _ := by
    ext
    simp
  map_smul' _
    _ := by
    ext
    simp

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