#
Homotopy Type Theory
rational function > history (Rev #1)

## Definition

Given a Heyting field $F$, let $f:F \to F$ and $g:F \to F$ be polynomial functions? and let $h:F_{#0} \to F$ be the reciprocal function of $F$. A rational function is a partial function

$k:\left(\sum{a:f} g(a) # 0\right) \to F$

defined as

$k(a) \coloneqq f(a) \cdot h(g(a))$

## See also

Revision on April 23, 2022 at 19:08:52 by
Anonymous?.
See the history of this page for a list of all contributions to it.