algebraMap_apply — Mathlib

English

The algebra map sends an element y to its underlying value: algebraMap(HomogeneousLocalization 𝒜 x, Localization x) y = y.val.

Русский

Алгебраическое отображение отправляет элемент y в его базовое значение: algebraMap(HomogeneousLocalization 𝒜 x, Localization x) y = y.val.

LaTeX

$$$\\mathrm{algebraMap}( \\mathrm{HomogeneousLocalization}(\\mathcal{A},x), \\mathrm{Localization}(x) )(y) = y.\\mathrm{val}$$$

Lean4

@[simp]
theorem algebraMap_apply (y) : algebraMap (HomogeneousLocalization 𝒜 x) (Localization x) y = y.val :=
  rfl

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