English
Distributing the product over addition in the index: (f+g).prod h = f.prod h · g.prod h under suitable additive hypotheses.
Русский
Разделение произведения по сложению внутри индекса: (f+g).prod h = f.prod h · g.prod h при надлежащих условиях.
LaTeX
$$(f + g).prod h = f.prod h * g.prod h$$
Lean4
@[to_additive]
theorem prod_add_index [∀ i, AddCommMonoid (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [CommMonoid γ] {f g : Π₀ i, β i}
{h : ∀ i, β i → γ} (h_zero : ∀ i, h i 0 = 1) (h_add : ∀ i b₁ b₂, h i (b₁ + b₂) = h i b₁ * h i b₂) :
(f + g).prod h = f.prod h * g.prod h :=
have f_eq : (∏ i ∈ f.support ∪ g.support, h i (f i)) = f.prod h :=
(Finset.prod_subset Finset.subset_union_left <| by simp +contextual [h_zero]).symm
have g_eq : (∏ i ∈ f.support ∪ g.support, h i (g i)) = g.prod h :=
(Finset.prod_subset Finset.subset_union_right <| by simp +contextual [h_zero]).symm
calc
(∏ i ∈ (f + g).support, h i ((f + g) i)) = ∏ i ∈ f.support ∪ g.support, h i ((f + g) i) :=
Finset.prod_subset support_add <| by simp +contextual [h_zero]
_ = (∏ i ∈ f.support ∪ g.support, h i (f i)) * ∏ i ∈ f.support ∪ g.support, h i (g i) := by {
simp [h_add, Finset.prod_mul_distrib]
}
_ = _ := by rw [f_eq, g_eq]
