isUnit_iff_norm_eq_one — Mathlib

English

An element of 𝒪[K] is a unit if and only if its norm equals 1.

Русский

Элемент 𝒪[K] является единицей тогда и только тогда, когда его норма равна 1.

LaTeX

$$$$ \text{IsUnit}(u) \iff \|u\| = 1, \quad u \in 𝒪[K] $$$$

Lean4

theorem isUnit_iff_norm_eq_one {u : 𝒪[K]} : IsUnit u ↔ ‖u‖ = 1 := by
  simpa [← NNReal.coe_inj] using
    (Valuation.integer.integers (NormedField.valuation (K := K))).isUnit_iff_valuation_eq_one

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