Definition quotient {p : prime_ideal R} (a : R) (b : prime_ideal_complement p) : localization_at p := prcommringfrac _ _ a b.
Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.MoreFoundations.Notations.