Field of Fractions

Stream: Is there code for X?

[Chris Hughes]

Do we have the field of fractions of an integral domain and the fact that the map is injective?

[Riccardo Brasca]

It should be docs#is_fraction_ring.injective

[Alex J. Best]

And https://leanprover-community.github.io/mathlib_docs/ring_theory/localization.html#fraction_ring for a construction

[Chris Hughes]

Thanks