mathlib

e20af159 - feat(field_theory): define the field of rational functions `ratfunc` (#9563)

feat(field_theory): define the field of rational functions `ratfunc` (#9563) This PR defines `ratfunc K` as the field of rational functions over a field `K`, in terms of `fraction_ring (polynomial K)`. I have been careful to use `structure`s and `@[irreducible] def`s. Not only does that make for a nicer API, it also helps quite a bit with unification since the check can stop at `ratfunc` and doesn't have to start unfolding along the lines of `fraction_field.field → localization.comm_ring → localization.comm_monoid → localization.has_mul` and/or `polynomial.integral_domain → polynomial.comm_ring → polynomial.ring → polynomial.semiring`. Most of the API is automatically derived from the (components of the) `is_fraction_ring` instance: the map `polynomial K → ratpoly K` is `algebra_map`, the isomorphism to `fraction_ring (polynomial K)` is `is_localization.alg_equiv`, ... As a first application to verify that the definitions work, I rewrote `function_field` in terms of `ratfunc`. Co-authored-by: Johan Commelin <johan@commelin.net>