prod_mul — Mathlib

English

The product over i of h1(i,b) h2(i,b) equals the product of the separate products.

Русский

Произведение по i от h1(i,b)h2(i,b) равно произведению по i от h1 и по i от h2.

LaTeX

$$$f.prod (\\\\lambda i b . h_1(i,b) * h_2(i,b)) = (f.prod h_1) * (f.prod h_2)$$$

Lean4

@[to_additive (attr := simp)]
theorem prod_mul [∀ i, AddCommMonoid (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [CommMonoid γ] {f : Π₀ i, β i}
    {h₁ h₂ : ∀ i, β i → γ} : (f.prod fun i b => h₁ i b * h₂ i b) = f.prod h₁ * f.prod h₂ :=
  Finset.prod_mul_distrib

Похожие утверждения