coeff' — Mathlib

English

The baseEmbedding combines all seeds into a partial linear map from baseDomain to Lex(HahnSeries).

Русский

baseEmbedding сочетает все seed-ы в частичное линейное отображение от baseDomain к Lex(HahnSeries).

LaTeX

$$$ seed.baseDomain \to Lex (HahnSeries (FiniteArchimedeanClass M) R) $$$

Lean4

/-- `HahnEmbedding.Seed.coeff` with `ArchimedeanStrata.stratum'` as domain. -/
def coeff' (c : ArchimedeanClass M) : seed.stratum' c →ₗ[K] R :=
  (seed.coeff c).comp (LinearMap.submoduleComap _ _)

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