Rational functions

Stream: new members

[Benjamin]

I am trying to write an algorithm in Lean that works with rational functions in two variables with integer coefficients. How can I represent such an object in Lean in a computable way? Does taking the FractionRing of a Polynomial work? And are there any differences between Polynomial and MvPolynomial that are relevant here?

[Benjamin]

(I didn't realize I was replying to an old thread when I wrote this.)

[Ruben Van de Velde]

Nothing related to Polynomial is "computable" in the lean sense

[Benjamin]

Does this include anything related to RatFunc?

[Ruben Van de Velde]

Yes

[Benjamin]

OK, so I will have to write my own implementation then?

[Kevin Buzzard]

I guess that depends on what you're doing. If it includes things like "put this ratio into canonical form by cancelling common factors" then I should think so, yes.

[Kevin Buzzard]

In lean right now we can do "prove (x^2-1)/(x+1)=x-1 by clearing denominators" but I doubt we can do "figure out a better normal form for (x^2-1)/(x+1)"