mathlib
53bd9d73 - feat(field_theory): generalize `ratfunc K` to `comm_ring K`/`is_domain K` (#10428)

Commit
4 years ago
feat(field_theory): generalize `ratfunc K` to `comm_ring K`/`is_domain K` (#10428) Fixes one of the TODO's from the original ratfunc PR: apply all the easy generalizations where `K` doesn't need to be a field, only a `is_domain K` or even just `comm_ring K`. This would allow us to use `ratfunc` in #10421.
Author
Parents
Loading