prodProdProdComm — Mathlib

English

There is a higher-arity isometry between nested products implementing a commutation.

Русский

Существует изометрия между вложенными произведениями, реализующая коммутативность.

LaTeX

$$IsometryEquiv.prodProdProdComm (Q1 Q2 Q3 Q4)$$

Lean4

/-- `LinearEquiv.prodProdProdComm` is isometric. -/
@[simps!]
def prodProdProdComm (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) (Q₃ : QuadraticMap R N₁ P)
    (Q₄ : QuadraticMap R N₂ P) : ((Q₁.prod Q₂).prod (Q₃.prod Q₄)).IsometryEquiv ((Q₁.prod Q₃).prod (Q₂.prod Q₄))
    where
  toLinearEquiv := LinearEquiv.prodProdProdComm _ _ _ _ _
  map_app' _ := add_add_add_comm _ _ _ _

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