algebraMap_adicCompletion

Mathlib.RingTheory.DedekindDomain.AdicValuation

URI: https://scilib.ai/kg/mathlib#IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion

English

Compatibility of the algebra map with adic completion maps.

Русский

Совместимость алгебраического отображения с отображениями adic завершения.

LaTeX

$$algebraMap_adicCompletion$$

Lean4

theorem algebraMap_adicCompletion : ⇑(algebraMap S <| v.adicCompletion K) = (↑) ∘ algebraMap S K :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru