English
For exps : HeightOneSpectrum(R) → ℤ, the valuation of a finitary product over w ≠ v of w^{exps w} is 0.
Русский
Для exps : HeightOneSpectrum(R) → ℤ, валуация произведения над w ≠ v из w^{exps w} равна 0.
LaTeX
$$$$ \\operatorname{count} \\bigl(K,v, \\prod_{w \\ne v}^{\\mathrm{finite}} w^{\\mathrm{exps}(w)}\\bigr) = 0. $$$$
Lean4
/-- `val_v(∏_{w ≠ v} w^{exps w}) = 0`. -/
theorem count_finprod_coprime (exps : HeightOneSpectrum R → ℤ) :
count K v (∏ᶠ (w : HeightOneSpectrum R) (_ : w ≠ v), (w.asIdeal : (FractionalIdeal R⁰ K)) ^ exps w) = 0 :=
by
apply finprod_mem_induction fun I => count K v I = 0
· exact count_one K v
· intro I I' hI hI'
classical
by_cases h : I ≠ 0 ∧ I' ≠ 0
· rw [count_mul' K v, if_pos h, hI, hI', add_zero]
· rw [count_mul' K v, if_neg h]
· intro w hw
rw [count_zpow, count_maximal_coprime K v hw, mul_zero]
