no goals
R : Type u_1
inst✝¹ : CommMonoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : { x // x ∈ S }
⊢ r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r₁ * r₂ /ₒ (s₁ * s₂)
rw [oreDiv_mul_char r₁ r₂ s₁ s₂ r₂ s₁ (by simp [mul_comm]), mul_comm s₂]
no goals
R : Type u_1
inst✝¹ : CommMonoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : { x // x ∈ S }
⊢ r₂ * ↑s₁ = ↑s₁ * r₂
simp [mul_comm]