linearMap — Mathlib

English

For each a in Γ, the map linearMap(a): V →ₗ[R] HahnSeries Γ V sends a vector v to the Hahn series whose coefficient at a is v and whose other coefficients are zero; this is an R-linear map.

Русский

Для каждого a ∈ Γ отображение linearMap(a): V →ₗ[R] HahnSeries Γ V отправляет вектор v в HahnSeries Γ V, у которого коэффициент при a равен v, а остальные коэффициенты нулевые; это линейное отображение по R.

LaTeX

$$$\\text{linearMap}(a) : V \\to_{R} HahnSeries(\\Gamma,V)$ — линейное отображение$$

Lean4

/-- `single` as a linear map -/
@[simps]
def linearMap (a : Γ) : V →ₗ[R] HahnSeries Γ V :=
  { single.addMonoidHom a with
    map_smul' := fun r s => by
      ext b
      by_cases h : b = a <;> simp [h] }

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