norm_eq_one_iff_notMem — Mathlib

English

The norm evaluated via the v-adic embedding equals 1 precisely when the element is not in the prime ideal.

Русский

Норма через вложение v-адической величины равна 1 тогда и только тогда, когда элемент не принадлежит идеалу.

LaTeX

$$$‖embedding\ v\ x‖ = 1 \iff x \notin v.asIdeal$$$

Lean4

/-- The `v`-adic norm of an integer is 1 if and only if it is not in the ideal. -/
theorem norm_eq_one_iff_notMem (x : 𝓞 (WithVal (v.valuation K))) : ‖embedding v x‖ = 1 ↔ x ∉ v.asIdeal :=
  by
  rw [norm_def]
  exact v.adicAbv_coe_eq_one_iff (one_lt_absNorm_nnreal v) x

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