algebraMap_adicCompletionIntegers_apply

English

The algebra map from R to the adic completion integers, applied to r, equals its image in the completion.

Русский

Алгебраическое отображение из R в adicCompletionIntegers_K_v, применённое к r, равно образу в завершении.

LaTeX

$$algebraMap R (v.adicCompletionIntegers K) r = (algebraMap R K r : v.adicCompletion K)$$

Lean4

@[simp]
theorem algebraMap_adicCompletionIntegers_apply (r : R) :
    algebraMap R (v.adicCompletionIntegers K) r = (algebraMap R K r : v.adicCompletion K) :=
  rfl

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