toPiLocalization_apply_apply — Mathlib

English

For any r in R and index I, the component of toPiLocalization at I equals the canonical algebra map of r.

Русский

Для любого элемента r в R и индекса I компонент toPiLocalization равен каноническому отображению по R в локализацию I.

LaTeX

$$$ (\mathrm{toPiLocalization}\ R\ r)\!\!_I = \mathrm{algebraMap}_{R\to R_I}(r) $$$

Lean4

theorem toPiLocalization_apply_apply {r I} : toPiLocalization R r I = algebraMap R _ r :=
  rfl

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