integer_valuation_le_one — Mathlib

English

For any x in S.integer K, the valuation at any place v not in S satisfies v.valuation_K(x) ≤ 1.

Русский

Для любого x ∈ S.integer K и любого места v, не принадлежащего S, выполняется v.valuation_K(x) ≤ 1.

LaTeX

$$$$\\forall x \\in S.integer K, \\forall v \\notin S,\\; v.valuation(K)(x) \\le 1$$$$

Lean4

theorem integer_valuation_le_one (x : S.integer K) {v : HeightOneSpectrum R} (hv : v ∉ S) : v.valuation K x ≤ 1 :=
  x.property v hv

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