Commit 2021-09-30 08:02 f76d0198

chore({field,ring}_theory): generalize fraction_ring and is_separable to rings (#9415) These used to be defined only for integral_domains resp. fields, however the construction makes sense even for comm_rings. 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, although the full test case is still quite slow (going from >40sec to approx 11 sec).