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.1326146
inst✝³ : CommRing R₁
K : Type ?u.1326152
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
y : P
h : spanSingleton S y = 0
⊢ span R {y} = ⊥
simpa using congr_arg Subtype.val h
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.1326146
inst✝³ : CommRing R₁
K : Type ?u.1326152
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
y : P
h : y = 0
⊢ spanSingleton S y = 0
simp [h]