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

Definiton

Given a commutative ring $R$ and a $R$-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

• module

• bilinear function

• Clifford algebra

• geometric algebra