ofPowerSeriesAlg — Mathlib

English

There is an algebra homomorphism from PowerSeries A to HahnSeries Γ A, giving a canonical passage of power series into Hahn series.

Русский

Существует гомоморфизм алгебр из PowerSeries A в HahnSeries Γ A, задающий канонический переход степенных рядов в ряды Хана.

LaTeX

$$$\\text{ofPowerSeriesAlg} : PowerSeries A \\to_{R} HahnSeries Γ A$ is an algebra homomorphism$$

Lean4

/-- Casting a power series as a Hahn series with coefficients from a `StrictOrderedSemiring`
  is an algebra homomorphism. -/
@[simps!]
def ofPowerSeriesAlg : PowerSeries A →ₐ[R] HahnSeries Γ A :=
  (HahnSeries.embDomainAlgHom (Nat.castAddMonoidHom Γ) Nat.strictMono_cast.injective fun _ _ => Nat.cast_le).comp
    (AlgEquiv.toAlgHom (toPowerSeriesAlg R).symm)

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