norm_lt_one_iff_mem — Mathlib

English

Let K be a number field, v a height-one place of the ring of integers, and x an element of the local ring at v. Then the v-adic norm of embedding v applied to x is less than 1 if and only if x lies in the ideal associated to v.

Русский

Пусть K — число поле, v — место высоты 1 в кольце целых 𝓞(K), а x ∈ 𝓞(WithVal(v.valuation K)). Тогда v-адиковая норма отображения embedding v(x) меньше 1 тогда и только тогда x принадлежит идеалу v.asIdeal.

LaTeX

$$$\\| \\mathrm{embedding}_v(x) \\| < 1 \\quad\\text{iff}\\quad x \\in v.asIdeal$$$

Lean4

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

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