no goals
R : Type ?u.1522445
inst✝⁷ : CommRing R
S : Submonoid R
P : Type ?u.1522652
inst✝⁶ : CommRing P
inst✝⁵ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_2
inst✝⁴ : CommRing R₁
K : Type u_1
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
x : K
h : x = 0
⊢ 1 / spanSingleton R₁⁰ x = spanSingleton R₁⁰ x⁻¹
simp [h]
no goals
R : Type ?u.1522445
inst✝⁷ : CommRing R
S : Submonoid R
P : Type ?u.1522652
inst✝⁶ : CommRing P
inst✝⁵ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_2
inst✝⁴ : CommRing R₁
K : Type u_1
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
x : K
h : ¬x = 0
⊢ spanSingleton R₁⁰ x * spanSingleton R₁⁰ x⁻¹ = 1
simp [h]