R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.3022378
inst✝¹ : CommRing P
K : Type ?u.3022384
inst✝ : IsLocalization M S
hM : M ≤ nonZeroDivisors R
⊢ ∀ (a : R), ↑(algebraMap R S) a = 0 → a = 0
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.3022378
inst✝¹ : CommRing P
K : Type ?u.3022384
inst✝ : IsLocalization M S
hM : M ≤ nonZeroDivisors R
⊢ Injective ↑(algebraMap R S)
rw [injective_iff_map_eq_zero (algebraMap R S)]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.3022378
inst✝¹ : CommRing P
K : Type ?u.3022384
inst✝ : IsLocalization M S
hM : M ≤ nonZeroDivisors R
a : R
ha : ↑(algebraMap R S) a = 0
⊢ a = 0
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.3022378
inst✝¹ : CommRing P
K : Type ?u.3022384
inst✝ : IsLocalization M S
hM : M ≤ nonZeroDivisors R
⊢ ∀ (a : R), ↑(algebraMap R S) a = 0 → a = 0
intro a ha
no goals
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.3022378
inst✝¹ : CommRing P
K : Type ?u.3022384
inst✝ : IsLocalization M S
hM : M ≤ nonZeroDivisors R
a : R
ha : ↑(algebraMap R S) a = 0
⊢ a = 0
rwa [to_map_eq_zero_iff S hM] at ha