R : Type ?u.1194138
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1194345
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I✝ J✝ I J : FractionalIdeal R₁⁰ K
h : J ≠ 0
x : K
⊢ x ∈ { val := ↑I / ↑J, property := (_ : IsFractional R₁⁰ (↑I / ↑J)) } ↔ ∀ (y : K), y ∈ J → x * y ∈ I
R : Type ?u.1194138
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1194345
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I✝ J✝ I J : FractionalIdeal R₁⁰ K
h : J ≠ 0
x : K
⊢ x ∈ I / J ↔ ∀ (y : K), y ∈ J → x * y ∈ I
rw [div_nonzero h]
no goals
R : Type ?u.1194138
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1194345
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I✝ J✝ I J : FractionalIdeal R₁⁰ K
h : J ≠ 0
x : K
⊢ x ∈ { val := ↑I / ↑J, property := (_ : IsFractional R₁⁰ (↑I / ↑J)) } ↔ ∀ (y : K), y ∈ J → x * y ∈ I
exact Submodule.mem_div_iff_forall_mul_mem