mk

Mathlib.NumberTheory.NumberField.FinitePlaces

URI: https://scilib.ai/kg/mathlib#NumberField.FinitePlace.mk

← MathLib Explorer

English

The norm along the embedding coincides with the v-adic norm on integers.

Русский

Норма вдоль вложения совпадает с v-адической нормой на целых.

LaTeX

$$$\|\mathrm{embedding}(v)\;x\| = \mathrm{adicAbv}(v,x)$$$

Lean4

/-- Return the finite place defined by a maximal ideal `v`. -/
noncomputable def mk (v : HeightOneSpectrum (𝓞 K)) : FinitePlace K :=
  ⟨place (embedding v), ⟨v, rfl⟩⟩

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

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

Разделы

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

Аффилиация

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