R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_1
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1298308
inst✝³ : CommRing R₁
K : Type ?u.1298314
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x y : P
⊢ x ∈ { val := span R {y}, property := (_ : IsFractional S (span R {y})) } ↔ ∃ z, z • y = x
R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_1
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1298308
inst✝³ : CommRing R₁
K : Type ?u.1298314
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x y : P
⊢ x ∈ spanSingleton S y ↔ ∃ z, z • y = x
rw [spanSingleton]
no goals
R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_1
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1298308
inst✝³ : CommRing R₁
K : Type ?u.1298314
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x y : P
⊢ x ∈ { val := span R {y}, property := (_ : IsFractional S (span R {y})) } ↔ ∃ z, z • y = x
exact Submodule.mem_span_singleton