embDomainLinearMap — Mathlib

English

Extending the domain of Hahn series with an order-embedding f yields a linear map from HahnSeries Γ R to HahnSeries Γ' R.

Русский

Расширение области Hahn series с помощью вложения порядка f дает линейное отображение от HahnSeries Γ R к HahnSeries Γ' R.

LaTeX

$$$\\text{embDomainLinearMap} (f) : HahnSeries(Γ,R) \\to_{L[R]} HahnSeries(Γ',R)$$$

Lean4

/-- Extending the domain of Hahn series is a linear map. -/
@[simps]
def embDomainLinearMap (f : Γ ↪o Γ') : HahnSeries Γ R →ₗ[R] HahnSeries Γ' R
    where
  toFun := embDomain f
  map_add' := embDomain_add f
  map_smul' := embDomain_smul f

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