linearMap — Mathlib

English

For each g in Γ, the map x ↦ coeff g (x) is an R-linear map from HahnSeries Γ V to V.

Русский

Для каждого элемента g ∈ Γ отображение x ↦ coeff g (x) является R-линейным отображением из HahnSeries Γ V в V.

LaTeX

$$$(\\text{coeff } g): HahnSeries(\\Gamma,V) \\to_{R} V \\text{ is linear}$$$

Lean4

/-- `coeff g` as a linear map -/
@[simps]
def linearMap (g : Γ) : HahnSeries Γ V →ₗ[R] V :=
  { coeff.addMonoidHom g with map_smul' := fun _ _ => rfl }

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