α : Type ?u.73822
β : Type ?u.73825
G : Type u_1
inst✝ : CommGroup G
a✝ b✝ c✝ d a b c : G
⊢ c / a * (a / b) = c / b
α : Type ?u.73822
β : Type ?u.73825
G : Type u_1
inst✝ : CommGroup G
a✝ b✝ c✝ d a b c : G
⊢ a / b * (c / a) = c / b
rw [mul_comm]
no goals
α : Type ?u.73822
β : Type ?u.73825
G : Type u_1
inst✝ : CommGroup G
a✝ b✝ c✝ d a b c : G
⊢ c / a * (a / b) = c / b
apply div_mul_div_cancel'