valuedAdicCompletion_def

Mathlib.RingTheory.DedekindDomain.AdicValuation

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

English

The valued structure on the adic completion is defined by extending the valuation to the completion.

Русский

Оценочная структура для завершения по адической норме задаётся через продолжение оценки к завершению.

LaTeX

$$Valued.valuedCompletion.v = valuation extension$$

Lean4

theorem valuedAdicCompletion_def {x : v.adicCompletion K} : Valued.v x = Valued.extension x :=
  rfl

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

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

Разделы

Аффилиация

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