English
As in the classical finiteness result, for any nonzero fractional ideal I the set of v with count(K,v,I) ≠ 0 is finite.
Русский
Как и в классическом конечном факторизации, для любого ненулевого дробного идеала I множество v с count(K,v,I) ≠ 0 конечно.
LaTeX
$$$\forall I \neq 0:\; (\{v: \mathrm{HeightOneSpectrum}(R) : \mathrm{count}(K,v,I) \neq 0\}).\mathrm{Finite}$.$$
Lean4
/-- `c.divMod b a` (i.e. `c / b mod a`) is an arbitrary `x` such that `c = bx + a`.
This is zero if the above is not possible, i.e. when `a = 0` or `b = 0` or `¬ a ≤ c`. -/
noncomputable def divMod (c b a : FractionalIdeal R⁰ K) : K :=
letI := Classical.propDecidable
if h : a ≤ c ∧ a ≠ 0 ∧ b ≠ 0 then (IsDedekindDomain.exists_add_spanSingleton_mul_eq h.1 h.2.1 h.2.2).choose else 0
