ofPowerSeries — Mathlib

English

The map ofPowerSeries from PowerSeries R to HahnSeries Γ R is injective for any Γ if R is semiring.

Русский

Отображение ofPowerSeries в HahnSeries Γ R инъективно при любых Γ, если R — полугруппа.

LaTeX

$$$ \text{ofPowerSeries}_{\Gamma, R} \text{ is injective} $$$

Lean4

/-- Casts a power series as a Hahn series with coefficients from a `StrictOrderedSemiring`. -/
def ofPowerSeries : PowerSeries R →+* HahnSeries Γ R :=
  (HahnSeries.embDomainRingHom (Nat.castAddMonoidHom Γ) Nat.strictMono_cast.injective fun _ _ => Nat.cast_le).comp
    (RingEquiv.toRingHom toPowerSeries.symm)

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