prodProdProdComm_toEquiv — Mathlib

English

The four-way product commutativity equivalence coincides with the canonical Equiv.prodProdProdComm.

Русский

Эквиваленция четырехкратной коммутативности произведений совпадает с канонической Equiv.prodProdProdComm.

LaTeX

$$$(prodProdProdComm\\ M\\ N\\ M'\\ N') : _ ≃ _ = Equiv.prodProdProdComm M N M' N'$$$

Lean4

@[to_additive (attr := simp) prodProdProdComm_toEquiv]
theorem prodProdProdComm_toEquiv : (prodProdProdComm M N M' N' : _ ≃ _) = Equiv.prodProdProdComm M N M' N' :=
  rfl

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