This is also defined in mathlib as Fraction Ring, which is the localisation at the non-zero divisors of your ring. When your ring $R$ is a commutative ring and an integral domain then gets the fact that this is a field.
Authors:
Knowl status:
- Review status: beta
- Last edited by Chris Birkbeck on 2025-10-23 10:59:39
Referred to by:
History:
(expand/hide all)
Differences
(show/hide)
Not referenced anywhere at the moment.