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