English
There is a natural isometry between dualProd on the product M×N and the product of dualProds: dualProd on M×N is isometric to dualProd M × dualProd N under the appropriate isomorphisms.
Русский
Существует естественная изометрия между dualProd на произведении M×N и произведением dualProd M и dualProd N.
LaTeX
$$dualProdProdIsometry : (dualProd R (M × N)) ≃ Isometry ((dualProd R M) × (dualProd R N))$$
Lean4
/-- `QuadraticForm.dualProd` commutes (isometrically) with `QuadraticForm.prod`. -/
@[simps!]
def dualProdProdIsometry : (dualProd R (M × N)).IsometryEquiv ((dualProd R M).prod (dualProd R N))
where
toLinearEquiv :=
(Module.dualProdDualEquivDual R M N).symm.prodCongr (LinearEquiv.refl R (M × N)) ≪≫ₗ
LinearEquiv.prodProdProdComm R _ _ M N
map_app' m := (m.fst.map_add _ _).symm.trans <| DFunLike.congr_arg m.fst <| Prod.ext (add_zero _) (zero_add _)
