English
The double- indexed product is commutative in the factors.
Русский
Двойное индексированное произведение симметрично по факторам.
LaTeX
$$$ f_1 .prod (\\\\lambda i_1 x_1 . f_2.prod (\\\\lambda i_2 x_2 . h i_1 x_1 i_2 x_2)) = f_2.prod (\\\\lambda i_2 x_2 . f_1.prod (\\\\lambda i_1 x_1 . h i_1 x_1 i_2 x_2)) $$$
Lean4
@[to_additive]
theorem prod_comm {ι₁ ι₂ : Sort _} {β₁ : ι₁ → Type*} {β₂ : ι₂ → Type*} [DecidableEq ι₁] [DecidableEq ι₂]
[∀ i, Zero (β₁ i)] [∀ i, Zero (β₂ i)] [∀ (i) (x : β₁ i), Decidable (x ≠ 0)] [∀ (i) (x : β₂ i), Decidable (x ≠ 0)]
[CommMonoid γ] (f₁ : Π₀ i, β₁ i) (f₂ : Π₀ i, β₂ i) (h : ∀ i, β₁ i → ∀ i, β₂ i → γ) :
(f₁.prod fun i₁ x₁ => f₂.prod fun i₂ x₂ => h i₁ x₁ i₂ x₂) =
f₂.prod fun i₂ x₂ => f₁.prod fun i₁ x₁ => h i₁ x₁ i₂ x₂ :=
Finset.prod_comm
