unit_valuation_eq_one — Mathlib

English

If x is an S-unit in K, then for every place v not in S, the v-adic valuation of x is 1 (trivial valuation).

Русский

Если x является S-единичным в K, то для каждой оценки v, не принадлежащей S, v-приближенная оценка x равна 1 (тривиальная).

LaTeX

$$$x\in S.\text{unit}(K)\Rightarrow \forall v\notin S: v.valuation(K)(x)=1$$$

Lean4

theorem unit_valuation_eq_one (x : S.unit K) {v : HeightOneSpectrum R} (hv : v ∉ S) : v.valuation K (x : Kˣ) = 1 :=
  x.property v hv

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