boxProdComm — Mathlib

English

Box product is commutative up to isomorphism: there exists a graph isomorphism between G □ H and H □ G given by Equiv.prodComm.

Русский

boxProd является коммутативным до изоморфизма: существует изоморфизм графов между G □ H и H □ G, задаваемый Equiv.prodComm.

LaTeX

$$$G \\Box H \\cong_g H \\Box G$$$

Lean4

/-- The box product is commutative up to isomorphism. `Equiv.prodComm` as a graph isomorphism. -/
@[simps!]
def boxProdComm : G □ H ≃g H □ G :=
  ⟨Equiv.prodComm _ _, or_comm⟩

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