Homotopy Type Theory reciprocal function > history (changes)

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

~~Definition~~

~~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~~

Heyting field

rational function

Last revised on June 10, 2022 at 17:51:18. See the history of this page for a list of all contributions to it.