coe_prodAssoc_symm — Mathlib

English

Symmetry of prodAssoc symmetry with respect to underlying function representation.

Русский

Симметрия симметрии prodAssoc относительно представления функции.

LaTeX

$$coe_prodAssoc_symm_deg : (prodAssoc R E E₂ E₃).symm = Equiv.prodAssoc E E₂ E₃$$

Lean4

@[simp]
theorem coe_prodAssoc_symm [Module R E₂] [Module R E₃] :
    ((prodAssoc R E E₂ E₃).symm : E × E₂ × E₃ → (E × E₂) × E₃) = (Equiv.prodAssoc E E₂ E₃).symm :=
  rfl

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