norm_coe_unit

Mathlib.Topology.Algebra.Valued.LocallyCompact

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

← MathLib Explorer

English

For any unit u in the valuation ring 𝒪[K], the norm of its image in K is 1.

Русский

Для любой единицы u в 𝒪[K], норма образа в K равна 1.

LaTeX

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

Lean4

@[simp]
theorem norm_coe_unit (u : 𝒪[K]ˣ) : ‖((u : 𝒪[K]) : K)‖ = 1 := by
  simpa [← NNReal.coe_inj] using (Valuation.integer.integers (NormedField.valuation (K := K))).valuation_unit u

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

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

Разделы

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

Аффилиация

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