prodProdProdComm_toLinearEquiv — Mathlib

English

The action of prodProdProdComm on a quadruple of elements rearranges them as specified.

Русский

Действие prodProdProdComm на кортеж четверки элементов переставляет их согласно заданному правилу.

LaTeX

$$$$ prodProdProdComm\, R\, M_1\, M_2\, M_3\, M_4 ((p_1, p_2), p_3, p_4) = ((p_1, p_3), p_2, p_4). $$$$

Lean4

@[simp]
theorem prodProdProdComm_toLinearEquiv :
    (prodProdProdComm R M₁ M₂ M₃ M₄).toLinearEquiv = LinearEquiv.prodProdProdComm R M₁ M₂ M₃ M₄ :=
  rfl

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