coe_algebraMap — Mathlib

English

There is a canonical algebra map from R⟦X⟧ to R⟨X⟩ given by HahnSeries.ofPowerSeries; in particular, the coercion (algebraMap) coincides with HahnSeries.ofPowerSeries.

Русский

Существует каноническое отображение алгебры из R⟦X⟧ в R⟨X⟩, заданное HahnSeries.ofPowerSeries; сопоставление совпадает с HahnSeries.ofPowerSeries.

LaTeX

$$$\text{algebraMap}_{R\langle X \rangle \to R}\; = \; \text{HahnSeries.ofPowerSeries } \mathbb{Z} R$$$

Lean4

@[simp]
theorem coe_algebraMap [CommSemiring R] : ⇑(algebraMap R⟦X⟧ R⸨X⸩) = HahnSeries.ofPowerSeries ℤ R :=
  rfl

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