coe_prodAssoc_symm — Mathlib

English

The underlying function of the symm of prodAssoc equals the inverse associativity swap.

Русский

Функционная часть симметричного prodAssoc равна обратной ассоциативной перестановке.

LaTeX

$$$\\mathrm{coe}(\\mathrm{prodAssoc}^{-1}) = (\\mathrm{Equiv.prodAssoc})^{-1}$$$

Lean4

@[to_additive (attr := simp) coe_prodAssoc_symm]
theorem coe_prodAssoc_symm : ⇑(prodAssoc : (M × N) × P ≃* M × (N × P)).symm = (Equiv.prodAssoc M N P).symm :=
  rfl

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