#
Homotopy Type Theory
reciprocal function > history (Rev #2, changes)

Showing changes from revision #1 to #2:
Added | ~~Removed~~ | ~~Chan~~ged

## Definition

< reciprocal function

~~Given a ~~

~~Heyting field~~~~ ~~~~$F$~~~~, let us define the type of all terms in ~~~~$F$~~~~ apart from 0:~~~~
~~$F_{#0} \coloneqq \left(\sum_{a:F} a # 0\right)$

~~
~~The **reciprocal function** is a partial function

~~
~~$f:F_{#0} \to F$

~~
~~with terms

~~
~~$\lambda:\prod_{a:F_{#0}} a \cdot f(a) = 1$

$\rho:\prod_{a:F_{#0}} f(a) \cdot a = 1$

~~
~~## See also

~~
~~
Revision on June 10, 2022 at 13:51:18 by
Anonymous?.
See the history of this page for a list of all contributions to it.