prodProdProdComm — Mathlib

English

A four-way commutativity isomorphism of products: (R × R') × S × S' ≃+* (R × S) × R' × S'.

Русский

Изоморфизм четырехкратного произведения: (R × R') × S × S' ≃+* (R × S) × R' × S'.

LaTeX

$$$ (R \\times R') \\times S \\times S' \\simeq+* (R \\times S) \\times R' \\times S'. $$$

Lean4

/-- Four-way commutativity of `Prod`. The name matches `mul_mul_mul_comm`. -/
@[simps apply]
def prodProdProdComm : (R × R') × S × S' ≃+* (R × S) × R' × S' :=
  { AddEquiv.prodProdProdComm R R' S S',
    MulEquiv.prodProdProdComm R R' S
      S' with
    toFun := fun rrss => ((rrss.1.1, rrss.2.1), (rrss.1.2, rrss.2.2))
    invFun := fun rsrs => ((rsrs.1.1, rsrs.2.1), (rsrs.1.2, rsrs.2.2)) }

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