English
An isometry between product-constructed quadratic maps can be formed from a pair of isometries on the left and right parts.
Русский
Изометрия между квадратичными формами, построенными через произведение, формируется из пары изометрий слева и справа.
LaTeX
$$def prod (e1: Q1.IsometryEquiv Q1') (e2: Q2.IsometryEquiv Q2') : (Q1.prod Q2).IsometryEquiv (Q1'.prod Q2')$$
Lean4
/-- An isometry between quadratic forms generated by `QuadraticForm.prod` can be constructed
from a pair of isometries between the left and right parts. -/
@[simps toLinearEquiv]
def prod {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P} {Q₁' : QuadraticMap R N₁ P} {Q₂' : QuadraticMap R N₂ P}
(e₁ : Q₁.IsometryEquiv Q₁') (e₂ : Q₂.IsometryEquiv Q₂') : (Q₁.prod Q₂).IsometryEquiv (Q₁'.prod Q₂')
where
map_app' x := congr_arg₂ (· + ·) (e₁.map_app x.1) (e₂.map_app x.2)
toLinearEquiv := LinearEquiv.prodCongr e₁.toLinearEquiv e₂.toLinearEquiv
