one_lt_absNorm_nnreal

Mathlib.NumberTheory.NumberField.FinitePlaces

URI: https://scilib.ai/kg/mathlib#NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm_nnreal

← MathLib Explorer

English

The valuation-related DVR property persists for adic completion substructures.

Русский

Свойство дискретной оценки сохраняется в подструктурах адик завершения.

LaTeX

$$$\text{IsDiscreteValuationRing}((v.adicCompletionK))$$$

Lean4

/-- The norm of a maximal ideal as an element of `ℝ≥0` is `> 1` -/
theorem one_lt_absNorm_nnreal : 1 < (absNorm v.asIdeal : ℝ≥0) :=
  mod_cast one_lt_absNorm v

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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