prod — Mathlib

English

An isometry between two quadratic maps built by taking products can be obtained from isometries of the left and right factors.

Русский

Изометрия между квадратичными формами, построенными как произведение, получается из изометрий левой и правой части.

LaTeX

$$Given isometries e1 and e2, (Q1.prod Q2) ≃ (Q1' .prod Q2') via IsometryEquiv.prod e1 e2.$$

Lean4

/-- Construct a quadratic form on a product of two modules from the quadratic form on each module.
-/
@[simps!]
def prod (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) : QuadraticMap R (M₁ × M₂) P :=
  Q₁.comp (LinearMap.fst _ _ _) + Q₂.comp (LinearMap.snd _ _ _)

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