English
For a finite index set s and a family of nonzero fractional ideals I_i, count(K, v, ∏_{i∈s} I_i) equals the sum over i∈s of count(K, v, I_i).
Русский
Для конечного множества индексов s и семейства ненулевых дробных идеалов I_i выполняется: count(K,v, ∏_{i∈s} I_i) = ∑_{i∈s} count(K,v, I_i).
LaTeX
$$$$ \\operatorname{count}\\bigl(K,v, \\prod_{i\\in s} I_i\\bigr) \\\\ = \\sum_{i\\in s} \\operatorname{count}(K,v,I_i). $$$$
Lean4
theorem count_prod {ι} (s : Finset ι) (I : ι → FractionalIdeal R⁰ K) (hS : ∀ i ∈ s, I i ≠ 0) :
count K v (∏ i ∈ s, I i) = ∑ i ∈ s, count K v (I i) := by
classical
induction s using Finset.induction with
| empty => rw [Finset.prod_empty, Finset.sum_empty, count_one]
| insert i s hi
hrec =>
have hS' : ∀ i ∈ s, I i ≠ 0 := fun j hj => hS j (Finset.mem_insert_of_mem hj)
have hS0 : ∏ i ∈ s, I i ≠ 0 := Finset.prod_ne_zero_iff.mpr hS'
have hi0 : I i ≠ 0 := hS i (Finset.mem_insert_self i s)
rw [Finset.prod_insert hi, Finset.sum_insert hi, count_mul K v hi0 hS0, hrec hS']
