English
An equality relating seed.hahnCoeff to the composed maps involving seed.hahnCoeff, seed.baseDomain, and the decomposition is satisfied.
Русский
Соответствие seed.hahnCoeff составным отображениям, включающим seed.baseDomain и разложение, соблюдено.
LaTeX
$$$ seed.hahnCoeff = ((DirectSum.lmap seed.coeff').comp (DirectSum.decomposeLinearEquiv seed.stratum').toLinearMap)$$$
Lean4
/-- Combining all `HahnEmbedding.Seed.coeff` as
a partial linear map from `HahnEmbedding.Seed.baseDomain` to `HahnSeries`. -/
noncomputable def baseEmbedding : M →ₗ.[K] Lex (HahnSeries (FiniteArchimedeanClass M) R)
where
domain := seed.baseDomain
toFun :=
(toLexLinearEquiv _ _).toLinearMap ∘ₗ
(HahnSeries.ofFinsuppLinearMap _) ∘ₗ
(Finsupp.lcomapDomain _ Subtype.val_injective) ∘ₗ (finsuppLequivDFinsupp K).symm.toLinearMap ∘ₗ seed.hahnCoeff
