English
Define val_v(I) for a fractional ideal I by choosing a representation I = a^{-1} J with a ∈ R and J an ideal, and setting val_v(I) = val_v(J) − val_v(a). If I = 0, then val_v(I) = 0.
Русский
Определим val_v(I) для дробного идеала I: если существует представление I = a^{-1} J с a ∈ R и J — идеал, тогда val_v(I) = val_v(J) − val_v(a). Если I = 0, то val_v(I) = 0.
LaTeX
$$$$\\mathrm{val}_v(I) := \\begin{cases} \\mathrm{val}_v(J) - \\mathrm{val}_v(a), & \\text{if } I = a^{-1}J, \\\\ 0, & \\text{if } I = 0. \\end{cases} $$$$
Lean4
/-- If `I` is a nonzero fractional ideal, `a ∈ R`, and `J` is an ideal of `R` such that `I = a⁻¹J`,
then we define `val_v(I)` as `(val_v(J) - val_v(a))`. If `I = 0`, we set `val_v(I) = 0`. -/
def count (I : FractionalIdeal R⁰ K) : ℤ :=
dite (I = 0) (fun _ : I = 0 => 0) fun _ : ¬I = 0 =>
let a := choose (exists_eq_spanSingleton_mul I)
let J := choose (choose_spec (exists_eq_spanSingleton_mul I))
((Associates.mk v.asIdeal).count (Associates.mk J).factors -
(Associates.mk v.asIdeal).count (Associates.mk (Ideal.span { a })).factors :
ℤ)
