mem_adicCompletionIntegers

Mathlib.RingTheory.DedekindDomain.AdicValuation

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

English

There exists an algebra structure on the adic completion extending the base ring action.

Русский

Существует структура алгебры над завершением по адической норме, расширяющая действие базового кольца.

LaTeX

$$instAlgebraAdicCompletion$$

Lean4

theorem mem_adicCompletionIntegers {x : v.adicCompletion K} : x ∈ v.adicCompletionIntegers K ↔ Valued.v x ≤ 1 :=
  Iff.rfl

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

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

Разделы

Аффилиация

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