coe_prodComm — Mathlib

English

The underlying function of the swap equivalence equals the canonical swap on the product, i.e., the function part of prodComm is swap.

Русский

Функциональная часть эквивалентности обмена совпадает с каноническим обменом на произведении; то есть функция prodComm равна swap.

LaTeX

$$$\\text{coe}(\\mathrm{prodComm}) = \\mathrm{Prod.swap}$$$

Lean4

@[to_additive (attr := simp) coe_prodComm]
theorem coe_prodComm : ⇑(prodComm : M × N ≃* N × M) = Prod.swap :=
  rfl

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