This file defines a bilinear form over a module. The definition requires a ring antiautomorphism on the scalar ring, which comes from the file ring_theory.involution. Basic ideas such as orthogonality are also introduced.
A sesquilinear form on an R-module M, is a function from M x M to R, that is linear in the first argument and antilinear in the second, with respect to an antiautomorphism on R (an antiisomorphism from R to R).
Given any term S of type sesq_form, due to a coercion, can use the notation S x y to refer to the function field, ie. S x y = S.bilin x y.
Sesquilinear form,
A sesquilinear form over a module
The proposition that two elements of a sesquilinear form space are orthogonal
The proposition that a sesquilinear form is reflexive
The proposition that a sesquilinear form is symmetric
The proposition that a sesquilinear form is alternating