adicAbv_def

Mathlib.NumberTheory.NumberField.FinitePlaces

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

English

The NNReal norm of a maximal ideal is strictly greater than 1.

Русский

NNReal-норма максимального идеала строго больше 1.

LaTeX

$$$1 < (\operatorname{absNorm}(v.asIdeal) : \mathbb{R}_{\ge 0})$$$

Lean4

theorem adicAbv_def {x : K} : adicAbv v x = toNNReal (absNorm_ne_zero v) (v.valuation K x) :=
  rfl

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

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

Разделы

Аффилиация

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