lsum — Mathlib

English

The sum operation for summable families defines a linear map from the family to the Hahn series.

Русский

Суммирование суммируемых семейств задаёт линейное отображение от семейства к гамма-рядам.

LaTeX

$$$ lsum : SummableFamily Γ R α \to HahnSeries Γ R $$$

Lean4

/-- The summation of a `summable_family` as a `LinearMap`. -/
@[simps]
def lsum : SummableFamily Γ R α →ₗ[HahnSeries Γ R] HahnSeries Γ R
    where
  toFun := hsum
  map_add' _ _ := hsum_add
  map_smul' _ _ := hsum_smul

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