rational functions

Stream: Is there code for X?

[Hunter Monroe]

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]

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

[Yury G. Kudryashov]

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

[Damiano Testa]

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]

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]

I would call it rational_functions F.

[Johan Commelin]

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]

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

[Hunter Monroe]

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

[Hunter Monroe]

(deleted)

[Hunter Monroe]

@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]

@Hunter Monroe #backticks

[Eric Wieser]

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

[Eric Wieser]

Does docs#fraction_ring exist?

[Adam Topaz]

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

[Adam Topaz]

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]

(deleted)