R : Type u_1
inst✝² : Ring R
S : Submonoid R
inst✝¹ : OreSet S
inst✝ : Nontrivial R
hS : S ≤ R⁰
h : 0 /ₒ 1 = 1 /ₒ 1
⊢ False
R : Type u_1
inst✝² : Ring R
S : Submonoid R
inst✝¹ : OreSet S
inst✝ : Nontrivial R
hS : S ≤ R⁰
h : 0 = 1
⊢ False
rw [OreLocalization.one_def, OreLocalization.zero_def] at h
no goals
R : Type u_1
inst✝² : Ring R
S : Submonoid R
inst✝¹ : OreSet S
inst✝ : Nontrivial R
hS : S ≤ R⁰
h : 0 /ₒ 1 = 1 /ₒ 1
⊢ False
apply nonZeroDivisors.coe_ne_zero 1 (numeratorHom_inj hS h).symm