English
For any nonzero fractional ideal I, the set of height-one spectrum v with count(K,v,I) ≠ 0 is finite; equivalently, count(K,v,I) = 0 for cofinitely many v.
Русский
Для любого ненулевого дробного идеала I множество высот-единиц v, таких что count(K,v,I) ≠ 0, конечно, конечно; эквивалентно count(K,v,I) = 0 для cofinitely многих v.
LaTeX
$$$\forall I \neq 0:\; \{v:\mathrm{HeightOneSpectrum}(R) : \mathrm{count}(K,v,I) \neq 0\} \text{ is finite}.$$$
Lean4
/-- `val_v(I) = 0` for all but finitely many maximal ideals of `R`. -/
theorem finite_factors (I : FractionalIdeal R⁰ K) : ∀ᶠ v : HeightOneSpectrum R in Filter.cofinite, count K v I = 0 :=
by
by_cases hI : I = 0
· simp only [hI, count_zero, Filter.eventually_cofinite, not_true_eq_false, setOf_false, finite_empty]
· convert finite_factors' hI (choose_spec (choose_spec (exists_eq_spanSingleton_mul I))).2
rw [count_ne_zero K _ hI]
