prodProdProdComm — Mathlib

English

Symmetry of the four-way product commutativity: (prodProdProdComm X Y W Z).symm = prodProdProdComm X W Y Z.

Русский

Симметрия четырехкратной перестановки произведений: (prodProdProdComm X Y W Z).symm = prodProdProdComm X W Y Z.

LaTeX

$$$(\mathrm{prodProdProdComm} X Y W Z).symm = \mathrm{prodProdProdComm} X W Y Z$$$

Lean4

/-- Four-way commutativity of `prod`. The name matches `mul_mul_mul_comm`. -/
def prodProdProdComm : (X × Y) × W × Z ≃ₜ (X × W) × Y × Z
    where
  toEquiv := Equiv.prodProdProdComm X Y W Z
  continuous_toFun := by
    unfold Equiv.prodProdProdComm
    dsimp only
    fun_prop
  continuous_invFun := by
    unfold Equiv.prodProdProdComm
    dsimp only
    fun_prop

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