## Definiton ## Let $A$, $B$, and $C$ be [[abelian group]]s, and let $f:A \times B \to C$ be a function from the product type of $A$ and $B$ to $C$. Let us define the types $$isLeftDistributive(f) \coloneqq \prod_{a:A} \prod_{b:B} \prod_{c:B} f(a, b +_B c) = f(a, b) +_C f(a, c)$$ $$isRightDistributive(f) \coloneqq \prod_{a:A} \prod_{b:A} \prod_{c:B} f(a +_A b, c) = f(a, c) +_C f(b, c)$$ $$isBilinear(f) \coloneqq isLeftDistributive(f) \times isRightDistributive(f)$$ $f$ is a __bilinear function__ if the type $isBilinear(f)$ has a term. We could define the type of all bilinear functions for abelian groups $A$, $B$, and $C$ as $$BilinearFunc(A, B, C) \prod_{f:A \times B \to C} isBilinear(f)$$ ## See also ## * [[abelian group]] * [[abelian group homomorphism]] * [[module]] * [[Z-algebra]] * [[quadratic form]] * [[trilinear function]]