algebraMap_def — Mathlib

English

The algebraMap from R to the completion of A equals the image of the algebraMap from R to A, embedded into the completion.

Русский

АлгебраMap из R в завершение A равен образу алгебраMap из R в A, затем встроенному в завершение.

LaTeX

$$$$ \mathrm{algebraMap}_{R}(\widehat{A})(r) = (\mathrm{algebraMap}_{R,A}(r))^{\wedge}, \quad r \in R $$$$

Lean4

theorem algebraMap_def (r : R) : algebraMap R (Completion A) r = (algebraMap R A r : Completion A) :=
  rfl

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