adicCompletion

Mathlib.RingTheory.DedekindDomain.AdicValuation

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

English

The completion of K with respect to the v-adic valuation is denoted v.valuation K).Completion.

Русский

Завершение K по v-адической оценке обозначается как v.valuation K).Completion.

LaTeX

$$Completion (v.valuation K)$$

Lean4

/-- The completion of `K` with respect to its `v`-adic valuation. -/
abbrev adicCompletion :=
  (v.valuation K).Completion

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

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

Разделы

Аффилиация

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