prodComm_symm — Mathlib

English

For all types α, β, the inverse of the swap equivalence is the swap with swapped types; i.e., the inverse of prodComm α β is prodComm β α.

Русский

Для всех типов α, β обратное к эквивалентности обмена является обменом с поменятыми типами; то есть prodComm α β^{-1} = prodComm β α.

LaTeX

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

Lean4

@[simp, grind =]
theorem prodComm_symm (α β) : (prodComm α β).symm = prodComm β α :=
  rfl

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