English
The v-adic valuation of r in a Dedekind domain is the exponent of v in the factorization of the principal ideal (r). If r = 0, by convention the valuation is 0.
Русский
V-адическая оценка элемента r в домене Дедекинд равна экспоненте v в факторизации идеала (r); если r = 0, по соглашению равна 0.
LaTeX
$$def intValuationDef (r : R) : ℤᵐ⁰ := if r = 0 then 0 else ↑(Multiplicative.ofAdd (-(Associates.mk v.asIdeal).count (Associates.mk (Ideal.span { r } : Ideal R)).factors : ℤ))$$
Lean4
/-- The additive `v`-adic valuation of `r ∈ R` is the exponent of `v` in the factorization of the
ideal `(r)`, if `r` is nonzero, or infinity, if `r = 0`. `intValuationDef` is the corresponding
multiplicative valuation. -/
def intValuationDef (r : R) : ℤᵐ⁰ :=
if r = 0 then 0
else
↑(Multiplicative.ofAdd (-(Associates.mk v.asIdeal).count (Associates.mk (Ideal.span { r } : Ideal R)).factors : ℤ))
