algebraMap_apply — Mathlib

English

For any r in R and A with an R-algebra structure, the image of r under the algebra map to HahnSeries Γ A equals the constant series with coefficient algebraMap_R^A r.

Русский

Для любого r ∈ R и A с структурой R-алгебры образ r в HahnSeries Γ A через алгебра-map равен константной серии с коэффициентом algebraMap_R^A(r).

LaTeX

$$$ \text{algebraMap}_R^{HahnSeries(\Gamma, A)}(r) = C(\text{algebraMap}_R^A(r)) $$$

Lean4

theorem algebraMap_apply {r : R} : algebraMap R (HahnSeries Γ A) r = C (algebraMap R A r) :=
  rfl

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