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