prodProdProdComm_symm — Mathlib

English

The inverse of the quadruple product commutes by swapping β and γ: mapping ((a,c),(b,d)) back to ((a,b),(c,d)).

Русский

Обратное четверной коммутации меняет местами β и γ: отображение ((a,c),(b,d)) обратно к ((a,b),(c,d)).

LaTeX

$$$$ (\\mathrm{prodProdProdComm}_{\\alpha,\\beta,\\gamma,\\delta})^{-1} = \\mathrm{prodProdProdComm}_{\\alpha,\\gamma,\\beta,\\delta}. $$$$

Lean4

@[simp, grind =]
theorem prodProdProdComm_symm (α β γ δ) : (prodProdProdComm α β γ δ).symm = prodProdProdComm α γ β δ :=
  rfl

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