norm_unit

Mathlib.Topology.Algebra.Valued.LocallyCompact

URI: https://scilib.ai/kg/mathlib#Valued.integer.norm_unit

English

The norm of a unit u in the valuation ring, viewed as an element of the ring itself, is 1.

Русский

Норма единицы u в кольце оценки равна 1.

LaTeX

$$$$ \|u\| = 1, \quad u \in 𝒪[K]^{\times} $$$$

Lean4

theorem norm_unit (u : 𝒪[K]ˣ) : ‖(u : 𝒪[K])‖ = 1 := by simp

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

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

Разделы

Аффилиация

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