mathlib
138c61fc - chore(field_theory/ratfunc): comm_ring (ratfunc K) (#11188)

Commit
4 years ago
chore(field_theory/ratfunc): comm_ring (ratfunc K) (#11188) Previously, the file only gave a `field (ratfunc K)` instance, requiring `comm_ring K` and `is_domain K`. In fact, `ratfunc K` is a `comm_ring` regardless of the `is_domain`. The upstream instance is proven first, with a generalized tactic.
Author
Parents
Loading