M : Type u_1
inst✝ : Group M
a b : M
ha : a ∈ center M
hb : b ∈ center M
⊢ a * b⁻¹ ∈ center M
M : Type u_1
inst✝ : Group M
a b : M
ha : a ∈ center M
hb : b ∈ center M
⊢ a / b ∈ center M
rw [div_eq_mul_inv]
no goals
M : Type u_1
inst✝ : Group M
a b : M
ha : a ∈ center M
hb : b ∈ center M
⊢ a * b⁻¹ ∈ center M
exact mul_mem_center ha (inv_mem_center hb)