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