coe_prodComm_symm — Mathlib

English

The symmetric of the four-way prod commutes back to the original: (prodProdComm R R' S S').symm = prodProdComm R S R' S'.

Русский

Обратное к четырехкратному смешению координат восстанавливает исходную перестановку: симметрия равна исходной.

LaTeX

$$$ (\\text{prodProdComm } R R' S S')^{-1} = \\text{prodProdComm } R S R' S'. $$$

Lean4

@[simp]
theorem coe_prodComm_symm : ⇑(prodComm : R × S ≃+* S × R).symm = Prod.swap :=
  rfl

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