Divisibility in localizations of commutative monoids

theorem Submonoid.LocalizationMap.map_isUnit_iff {M : Type u_1} {N : Type u_2} [CommMonoid M] {S : Submonoid M} [CommMonoid N] (f : S.LocalizationMap N) {m : M} : IsUnit (f m) ↔ ∃ s ∈ S, m ∣ s

theorem Submonoid.LocalizationMap.map_dvd_map {M : Type u_1} {N : Type u_2} [CommMonoid M] {S : Submonoid M} [CommMonoid N] (f : S.LocalizationMap N) {m₁ m₂ : M} : f m₁ ∣ f m₂ ↔ ∃ s ∈ S, m₁ ∣ s * m₂