∀ {A : Type u_1} (K : Type u_2) [inst : CommRing A] (S : Submonoid A) (hS : S ≤ nonZeroDivisors A) [inst_1 : CommRing K]
  [inst_2 : Algebra A K] [inst_3 : IsFractionRing A K], IsFractionRing (↥(Localization.subalgebra K S hS)) K