English
The natural rearrangement of a fourfold product is compatible with the standard product equivalence. In particular, the continuous linear equivalence corresponding to rearranging ((M1×M2)×M3)×M4 is the same as the standard Equiv.prodProdProdComm.
Русский
Естественное преобразование перестановки четырехфакторного произведения совместимо с стандартной эквивалентностью произведений. В частности, эквивалентность, соответствующая перестановке ((M1×M2)×M3)×M4, совпадает с обычной эквивалентностью Equiv.prodProdProdComm.
LaTeX
$$$ContinuousLinearEquiv.prodProdProdComm(R,M_1,M_2,M_3,M_4) = Equiv.prodProdProdComm(M_1,M_2,M_3,M_4)$$$
Lean4
@[simp]
theorem coe_prodProdProdComm :
(prodProdProdComm R M₁ M₂ M₃ M₄ : (M₁ × M₂) × M₃ × M₄ → (M₁ × M₃) × M₂ × M₄) = Equiv.prodProdProdComm M₁ M₂ M₃ M₄ :=
rfl
