M : Type u_1
S T : Set M
a b : M
inst✝ : GroupWithZero M
ha : a ∈ centralizer S
hb : b ∈ centralizer S
⊢ a * b⁻¹ ∈ centralizer S
M : Type u_1
S T : Set M
a b : M
inst✝ : GroupWithZero M
ha : a ∈ centralizer S
hb : b ∈ centralizer S
⊢ a / b ∈ centralizer S
rw [div_eq_mul_inv]
no goals
M : Type u_1
S T : Set M
a b : M
inst✝ : GroupWithZero M
ha : a ∈ centralizer S
hb : b ∈ centralizer S
⊢ a * b⁻¹ ∈ centralizer S
exact mul_mem_centralizer ha (inv_mem_centralizer₀ hb)