coe_algebraMap — Mathlib

English

The algebra map from R to LocallyConstant(X,Y) is compatible with evaluation, i.e., its image as a function is the same as the corresponding algebra map to X→Y.

Русский

Алгебраическая карта из R в LocallyConstant(X,Y) согласуется с вычислением по точкам: ее образ как функция совпадает с алгебраической картой в X→Y.

LaTeX

$$$\operatorname{algebraMap}_R(\operatorname{LocallyConstant}(X,Y))\, r = \operatorname{algebraMap}_R(X\to Y)\, r$$$

Lean4

@[simp]
theorem coe_algebraMap (r : R) : ⇑(algebraMap R (LocallyConstant X Y) r) = algebraMap R (X → Y) r :=
  rfl

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