no goals
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r r' : R
s : { x // x ∈ S }
⊢ r /ₒ s + r' /ₒ s = (r + r') /ₒ s
simp [oreDiv_add_char s s 1 1 (by simp)]
no goals
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r r' : R
s : { x // x ∈ S }
⊢ ↑s * ↑1 = ↑s * 1
simp