prodComm — Mathlib

English

The swapped product equality preserves isometry via prodComm.

Русский

Перестановка факторов сохраняет изометричность через prodComm.

LaTeX

$$IsometryEquiv.prodComm {Q1} {Q2} : (Q1.prod Q2) IsometryEquiv (Q2.prod Q1)$$

Lean4

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

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