prodAssoc_symm_apply — Mathlib

English

The inverse of prodAssoc acts by reversing the nesting: (prodAssoc R M1 M2 M3)^{-1} (p1, (p2, p3)) = ((p1, p2), p3).

Русский

Обратное к prodAssoc действует, разворачивая вложения: (prodAssoc R M1 M2 M3)^{-1} (p1, (p2, p3)) = ((p1, p2), p3).

LaTeX

$$$$ (prodAssoc\, R\, M_1\, M_2\, M_3)^{-1} (p_1, (p_2, p_3)) = ((p_1, p_2), p_3). $$$$

Lean4

@[simp]
theorem prodAssoc_symm_apply (p₁ : M₁) (p₂ : M₂) (p₃ : M₃) :
    (prodAssoc R M₁ M₂ M₃).symm (p₁, (p₂, p₃)) = ((p₁, p₂), p₃) :=
  rfl

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