adicAbv

Mathlib.NumberTheory.NumberField.FinitePlaces

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

← MathLib Explorer

English

The norm of a maximal ideal, as a nonnegative real, is nonzero.

Русский

Норма максимального идеала в NNReal не равна нулю.

LaTeX

$$$\operatorname{absNorm}(v.asIdeal)\neq 0$$$

Lean4

/-- The `v`-adic absolute value on `K` defined as the norm of `v` raised to negative `v`-adic
valuation -/
noncomputable def adicAbv : AbsoluteValue K ℝ :=
  v.adicAbv <| one_lt_absNorm_nnreal v

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

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

Разделы

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

Аффилиация

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