prod_comm — Mathlib

English

For finsupps f : α →₀ M and g : β →₀ M', and any h : α → M → β → M' → N, the product is symmetric in the two factors: (f.prod (λ x v, g.prod (λ x' v', h x v x' v'))) = (g.prod (λ x' v', f.prod (λ x v, h x v x' v))).

Русский

Для двух фрагментов Finsupp есть симметрия произведения: prod в одном порядке равен prod в другом порядке.

LaTeX

$$$ f \\to_{prod} g = g \\to_{prod} f $$$

Lean4

@[to_additive]
theorem prod_comm (f : α →₀ M) (g : β →₀ M') (h : α → M → β → M' → N) :
    (f.prod fun x v => g.prod fun x' v' => h x v x' v') = g.prod fun x' v' => f.prod fun x v => h x v x' v' :=
  Finset.prod_comm

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