case c
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r✝ : R
s✝ : { x // x ∈ S }
⊢ 0 + r✝ /ₒ s✝ = r✝ /ₒ s✝
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
x : OreLocalization R S
⊢ 0 + x = x
induction x using OreLocalization.ind
case c
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r✝ : R
s✝ : { x // x ∈ S }
⊢ (0 + r✝) /ₒ s✝ = r✝ /ₒ s✝
case c
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r✝ : R
s✝ : { x // x ∈ S }
⊢ 0 + r✝ /ₒ s✝ = r✝ /ₒ s✝
rw [← zero_div_eq_zero, add_oreDiv]
no goals
case c
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r✝ : R
s✝ : { x // x ∈ S }
⊢ (0 + r✝) /ₒ s✝ = r✝ /ₒ s✝
simp