This file defines a bilinear form over a module. Basic ideas such as orthogonality are also introduced, as well as reflexivive, symmetric and alternating bilinear forms.
A bilinear form on an R-module V, is a function from V x V to R, that is linear in both arguments
Given any term B of type bilin_form, due to a coercion, can use the notation B x y to refer to the function field, ie. B x y = B.bilin x y.
Bilinear form,
A bilinear form over a module
The proposition that two elements of a bilinear form space are orthogonal
The proposition that a bilinear form is reflexive
The proposition that a bilinear form is symmetric
The proposition that a bilinear form is alternating