prodProdProdComm_symm — Mathlib

English

Symmetry of the four-way product-commuting isomorphism under swapping the middle blocks.

Русский

Симметрия четырехкратного коммутативного изоморфа произведения при перестановке средних блоков.

LaTeX

$$$(\mathrm{prodProdProdComm} \ R\ M M_2 M_3 M_4).\mathrm{symm} = \mathrm{prodProdProdComm} \ R\ M M_3 M_2 M_4$$$

Lean4

@[simp]
theorem prodProdProdComm_symm : (prodProdProdComm R M M₂ M₃ M₄).symm = prodProdProdComm R M M₃ M₂ M₄ :=
  rfl

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