English
There is a multiplicative equivalence that rearranges a quadruple ((M × N) × M' × N') into ((M × M') × N × N'), reflecting four-way commutativity of product.
Русский
Существует мультипликативное эквивалентное отображение, переставляющее квадруплекс (M × N) × M' × N' в (M × M') × N × N', отражая четырехкратное коммутативное свойство произведения.
LaTeX
$$$\\text{prodProdProdComm} : (M \\times N) \\times M' \\times N' \\simeq_* (M \\times M') \\times N \\times N'.$$$
Lean4
/-- Four-way commutativity of `Prod`. The name matches `mul_mul_mul_comm`. -/
@[to_additive (attr := simps apply) prodProdProdComm /-- Four-way commutativity of `Prod`.
The name matches `mul_mul_mul_comm` -/
]
def prodProdProdComm : (M × N) × M' × N' ≃* (M × M') × N × N' :=
{
Equiv.prodProdProdComm M N M'
N' with
toFun := fun mnmn => ((mnmn.1.1, mnmn.2.1), (mnmn.1.2, mnmn.2.2))
invFun := fun mmnn => ((mmnn.1.1, mmnn.2.1), (mmnn.1.2, mmnn.2.2))
map_mul' := fun _mnmn _mnmn' => rfl }
