Homotopy Type Theory quadratic form > history (Rev #3, changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

Definiton

Given a commutative ring $R$ and a $R$- bimodule module $B$, a quadratic form is a function $q:B \to R$ such that the binary function $r:B \times B \to R$ pointwise defined as

is a bilinear function, and for $a:R$ and $v:B$, $p(a, v): q(a v) = a^2 q(v)$.

See also

• bimodule module

• bilinear function

• Clifford algebra

• geometric algebra