tprod_comm — Mathlib

English

The tprod is invariant under swapping the order: under a suitable Multipliable condition on Function.uncurry f, ∏' c b f b c = ∏' b c f b c.

Русский

Произведение по двум переменным не зависит от порядка перемножения при условии множимости.

LaTeX

$$$\\prod' (c) (b), f b c = \\prod' (b) (c), f b c$$$

Lean4

@[to_additive]
protected theorem tprod_comm {f : β → γ → α} (h : Multipliable (Function.uncurry f)) :
    ∏' (c) (b), f b c = ∏' (b) (c), f b c :=
  h.tprod_comm' h.prod_factor h.prod_symm.prod_factor

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