∀ {R : Type u_3} [inst : CommRing R] {M : Submonoid R} (S : Type u_4) [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [IsLocalization M S], M ≤ nonZeroDivisors R → Function.Injective (IsLocalization.coeSubmodule S)