English
The additive analogue holds: for any abelian additive monoid α and f: InfinitePlace(K) → α, sum over all places equals sum over real places plus sum over complex places.
Русский
Аналог с суммированием: для любой абелевой аддитивной моноиды α и функции f: InfinitePlace(K) → α выполняется равенство сумм по всем местам равно сумме по реальным местам плюс сумме по комплексным местам.
LaTeX
$$$\\forall f : \\mathrm{InfinitePlace}(K) \\to \\alpha,\\quad \\sum_{w} f(w) = \\left(\\sum_{w \in \\{ w : \\mathrm{InfinitePlace}(K) \\mid \\mathrm{IsReal} w \\}} f(w)\\right) + \\left(\\sum_{w \\in \\{ w : \\mathrm{InfinitePlace}(K) \\mid \\mathrm{IsComplex} w \\}} f(w)\\right)$$$
Lean4
@[to_additive]
theorem prod_eq_prod_mul_prod {α : Type*} [CommMonoid α] [NumberField K] (f : InfinitePlace K → α) :
∏ w, f w = (∏ w : { w // IsReal w }, f w.1) * (∏ w : { w // IsComplex w }, f w.1) :=
by
rw [← Equiv.prod_comp (Equiv.subtypeEquivRight (fun _ ↦ not_isReal_iff_isComplex))]
simp [Fintype.prod_subtype_mul_prod_subtype]
