prodAssoc_toLinearEquiv — Mathlib

English

The CLEx prodAssoc corresponds to the standard linear equivalence prodAssoc on tuples.

Русский

CLEx prodAssoc соответствует стандартному линейному эквиваленту prodAssoc на кортежах.

LaTeX

$$$$ (prodAssoc\, R\, M_1\, M_2\, M_3).toLinearEquiv = LinearEquiv.prodAssoc\, R\, M_1\, M_2\, M_3. $$$$

Lean4

@[simp]
theorem prodAssoc_toLinearEquiv : (prodAssoc R M₁ M₂ M₃).toLinearEquiv = LinearEquiv.prodAssoc R M₁ M₂ M₃ :=
  rfl

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