Commit 2021-11-16 12:48 e20af159

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 structures and @[irreducible] defs. 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.