English
For a fixed height-one place v, the v-adic valuation on K× is defined by localization at v, taking into account the exponents of the numerator and denominator in the associated ideals, resulting in a homomorphism to Multiplicative Z.
Русский
Для фиксированного места высоты один v-адическая ценность на K× задаётся локализацией в v, с учётом степеней множителей числителя и знаменателя в ассоциированных идеалах, получая однородную отображение в Multiplicative Z.
LaTeX
$$$\text{valuation}_{v}:K^{\times}\to \operatorname{Multiplicative}(\mathbb{Z})$$$
Lean4
/-- The multiplicative `v`-adic valuation on `Kˣ`. -/
def valuationOfNeZeroToFun (x : Kˣ) : Multiplicative ℤ :=
let hx := IsLocalization.sec R⁰ (x : K)
Multiplicative.ofAdd <|
(-(Associates.mk v.asIdeal).count (Associates.mk <| Ideal.span { hx.fst }).factors : ℤ) -
(-(Associates.mk v.asIdeal).count (Associates.mk <| Ideal.span {(hx.snd : R)}).factors : ℤ)
