R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I : FractionalIdeal S P
x : P
hx : x ∈ 0
⊢ x ∈ I
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I : FractionalIdeal S P
⊢ 0 ≤ I
intro x hx
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I : FractionalIdeal S P
x : P
hx : x ∈ 0
⊢ 0 ∈ I
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I : FractionalIdeal S P
x : P
hx : x ∈ 0
⊢ x ∈ I
rw [(mem_zero_iff _).mp hx]
no goals
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I : FractionalIdeal S P
x : P
hx : x ∈ 0
⊢ 0 ∈ I
exact zero_mem (I : Submodule R P)