mathlib

f76d0198 - chore({field,ring}_theory): generalize `fraction_ring` and `is_separable` to rings (#9415)

chore({field,ring}_theory): generalize `fraction_ring` and `is_separable` to rings (#9415) These used to be defined only for `integral_domain`s resp. `field`s, however the construction makes sense even for `comm_ring`s. So we can just do the generalization for free, and moreover it makes certain proof terms in their definition a lot smaller. Together with #9414, this helps against [timeouts when combining `localization` and `polynomial`](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60variables.60.20doesn't.20time.20out.20but.20inline.20params.20do), although the full test case is still quite slow (going from >40sec to approx 11 sec).