## Stream: Is there code for X?

### Topic: rational functions

#### Hunter Monroe (Apr 12 2021 at 18:27):

Is there code for rational functions? It appears on the page for missing undergrad math and is not in the PR list or issues. I would like to add code for rational functions--any reactions? For the definition, what would be a good name , e.g., ratfunc? What should this code cover? I suggest: identifying domain and range of rational functions, definition of horizontal, vertical, and slant asymptotes using limits, formula for asymptotes.

#### Yury G. Kudryashov (Apr 12 2021 at 18:35):

Probably you should start with purely algebraic definition (e.g., as the field of fractions of polynomial R).

#### Yury G. Kudryashov (Apr 12 2021 at 18:36):

Once this is merged, you can prove something about limits etc.

#### Damiano Testa (Apr 12 2021 at 18:57):

There is something about localizations in the file ring_theory/localization. In particular, I think that it defines a localization of an integral domain at the multiplicative submonoid of all the non-zero elements as fraction_map R K. I hope that this could be a beginning!

#### Hunter Monroe (Apr 13 2021 at 04:48):

OK, for full generality, given a field F, and polynomials over elements of F which form a ring R, we define polynomial_fraction_ring , as "fraction_ring R" with Type u_4. And then a rational function would be any element of that. This would be a new definition in ring_theory.localization. Is that roughly what you are suggesting?

#### Johan Commelin (Apr 13 2021 at 05:14):

I would call it rational_functions F.

#### Johan Commelin (Apr 13 2021 at 05:14):

And it doesn't have to be defined that way. You can also define it in a hands-on manner. But it will be important that you provide localization (polynomial F) (rational_function F).

#### Johan Commelin (Apr 13 2021 at 05:15):

Because once you have done that, you can start treating it as a localization, which unlocks a nice library for you.

#### Hunter Monroe (Apr 13 2021 at 05:23):

Johan Commelin said:

Because once you have done that, you can start treating it as a localization, which unlocks a nice library for you.

OK makes sense Johan, thanks

(deleted)

#### Hunter Monroe (Apr 17 2021 at 14:44):

@Johan Commelin am I heading in the right direction and what is needed for the last line?

import data.polynomial.basic
import ring_theory.localization
universes u
variables {R : Type u}
namespace polynomial
variable [comm_ring R]
variables {p : polynomial R}
def rational_functions : fraction_ring p
end polynomial


#### Adam Topaz (Apr 17 2021 at 14:51):

@Hunter Monroe #backticks

#### Eric Wieser (Apr 17 2021 at 14:54):

The syntax is def name : type := value, your def is missing the :=

#### Eric Wieser (Apr 17 2021 at 14:55):

Does docs#fraction_ring exist?

#### Adam Topaz (Apr 17 2021 at 14:55):

Yes, but note that it takes a ring as an input, not a polynomial.

#### Adam Topaz (Apr 17 2021 at 14:56):

You probably want something of the following form:

import data.polynomial.basic
import ring_theory.localization

variables (k : Type*) [field k]

def rational_function_field_in_one_variable :=
fraction_ring (polynomial k)


(and probably a better name than I came up with :smile: )

#### Eric Wieser (Apr 17 2021 at 20:28):

(deleted)

Last updated: May 16 2021 at 05:21 UTC