English
There is a natural equivalence between (α × β) × γ × δ and (α × γ) × β × δ given by rearranging the components: ((a,b), (c,d)) maps to ((a,c), (b,d)).
Русский
Существуют естественная эквивалентность между (α × β) × γ × δ и (α × γ) × β × δ, заданная перераспределением компонентов: ((a,b),(c,d)) ↦ ((a,c),(b,d)).
LaTeX
$$$$ ((a,b),(c,d)) \\mapsto ((a,c),(b,d)). $$$$
Lean4
/-- Four-way commutativity of `prod`. The name matches `mul_mul_mul_comm`. -/
@[simps (attr := grind =) apply]
def prodProdProdComm (α β γ δ) : (α × β) × γ × δ ≃ (α × γ) × β × δ
where
toFun abcd := ((abcd.1.1, abcd.2.1), (abcd.1.2, abcd.2.2))
invFun acbd := ((acbd.1.1, acbd.2.1), (acbd.1.2, acbd.2.2))
