truncLTLinearMap — Mathlib

English

For a fixed c ∈ Γ, truncLTLinearMap[c] gives a linear map that truncates Hahn series below c, i.e., keeps only terms with exponent less than c.

Русский

Для фиксированного c ∈ Γ, truncLTLinearMap[c] задает линейное отображение, усекающее ряд Хана ниже c, то есть сохраняет только термы с показателями меньше c.

LaTeX

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

Lean4

/-- `HahnSeries.truncLT` as a linear map. -/
def truncLTLinearMap [DecidableLT Γ] (c : Γ) : HahnSeries Γ V →ₗ[R] HahnSeries Γ V
    where
  toFun := truncLT c
  map_add' := truncLT_add c
  map_smul' := truncLT_smul c

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