R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.370358
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
z : S
x : R
y : { x // x ∈ M }
h : z * ↑(algebraMap R S) ↑y = 0
hx : x = 0
⊢ z = 0
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.370358
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
z : S
x : R
y : { x // x ∈ M }
h : z * ↑(algebraMap R S) ↑y = ↑(algebraMap R S) x
hx : x = 0
⊢ z = 0
rw [hx, (algebraMap R S).map_zero] at h
no goals
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.370358
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
z : S
x : R
y : { x // x ∈ M }
h : z * ↑(algebraMap R S) ↑y = 0
hx : x = 0
⊢ z = 0
exact (IsUnit.mul_left_eq_zero (IsLocalization.map_units S y)).1 h