no goals
A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝² : CommRing K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
hS : S ≤ A⁰
s : { x // x ∈ S }
⊢ IsUnit (↑(algebraMap A K) ↑s)
apply IsLocalization.map_units K (⟨s.1, hS s.2⟩ : A⁰)