English
There is an isometry between the quadratic form dualProd on M and the product of Q and its negation, i.e., the dualProd on M is isometric to the product Q × (-Q).
Русский
Существует изометрия между квадратичной формой dualProd на M и произведением Q и −Q; dualProd на M эквивалентна произведению Q × (−Q).
LaTeX
$$$ dualProd\\ R\\ M \\cong Isometry\\left( Q, -Q \\right) $$$
Lean4
/-- The symmetric bilinear form on `Module.Dual R M × M` defined as
`B (f, x) (g, y) = f y + g x`. -/
@[simps!]
def dualProd : LinearMap.BilinForm R (Module.Dual R M × M) :=
(applyₗ.comp (snd R (Module.Dual R M) M)).compl₂ (fst R (Module.Dual R M) M) +
((applyₗ.comp (snd R (Module.Dual R M) M)).compl₂ (fst R (Module.Dual R M) M)).flip
