algebraMap_apply' — Mathlib

English

Compatibility of the algebra maps: applying the S-algebra map to an element x matches applying via the ofPowerSeries construction to the corresponding PowerSeries image.

Русский

Совместимость отображений алгебры: применение algebraMap_S к x совпадает с применением через конструкцию ofPowerSeries к образу в PowerSeries.

LaTeX

$$$\\ algebraMap_S( HahnSeries Γ R)\\, x = \\ operatorname{ofPowerSeries}_{\\Gamma,R}(\\ algebraMap_S( PowerSeries R)\\, x)$$$

Lean4

theorem algebraMap_apply' (x : S) :
    algebraMap S (HahnSeries Γ R) x = ofPowerSeries Γ R (algebraMap S (PowerSeries R) x) :=
  rfl

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