Homotopy Type Theory rational function > history (changes)

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

Definition

< rational function

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

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