English
For f : α ⊕ β → M where M is a commutative monoid with topology and multiplication, the tprod over α ⊕ β equals the product of the tprod over α and over β, provided each side is Multipliable.
Русский
Для f : α ⊕ β → M, т-продукт по всему α ⊕ β равен произведению т-продуктов по α и по β, если обе стороны сходятся.
LaTeX
$$$(h_1: Multipliable (f \\circ Sum.inl)) (h_2: Multipliable (f \\circ Sum.inr)) : \\\\prod' i, f i = (\\prod' i, f (Sum.inl i)) \\cdot (\\prod' i, f (Sum.inr i))$$$
Lean4
@[to_additive /-- For the statement that `tsum` commutes with `Finset.sum`,
see `Summable.tsum_finsetSum`. -/
]
protected theorem tprod_sum {α β M : Type*} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] [T2Space M]
{f : α ⊕ β → M} (h₁ : Multipliable (f ∘ .inl)) (h₂ : Multipliable (f ∘ .inr)) :
∏' i, f i = (∏' i, f (.inl i)) * (∏' i, f (.inr i)) :=
(h₁.hasProd.sum h₂.hasProd).tprod_eq
