prod_comm_cycle — Mathlib

English

Cyclically permute three nested finite products: ∏_{x ∈ s} ∏_{y ∈ t} ∏_{z ∈ u} f(x,y,z) = ∏_{z ∈ u} ∏_{x ∈ s} ∏_{y ∈ t} f(x,y,z).

Русский

Циклически переставим три вложенных произведения: ∏_{x ∈ s} ∏_{y ∈ t} ∏_{z ∈ u} f(x,y,z) = ∏_{z ∈ u} ∏_{x ∈ s} ∏_{y ∈ t} f(x,y,z).

LaTeX

$$$$\\prod_{x \\in s} \\prod_{y \\in t} \\prod_{z \\in u} f(x,y,z) = \\prod_{z \\in u} \\prod_{x \\in s} \\prod_{y \\in t} f(x,y,z). $$$$

Lean4

/-- Cyclically permute 3 nested instances of `Finset.prod`. -/
@[to_additive]
theorem prod_comm_cycle {s : Finset γ} {t : Finset α} {u : Finset κ} {f : γ → α → κ → β} :
    (∏ x ∈ s, ∏ y ∈ t, ∏ z ∈ u, f x y z) = ∏ z ∈ u, ∏ x ∈ s, ∏ y ∈ t, f x y z := by
  simp_rw [prod_comm (s := t), prod_comm (s := s)]

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