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

Showing changes from revision #0 to #1: Added | Removed | Changed

Definition

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

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

defined as

k(a)f(a)h(g(a))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.