M : Type u_1
S T : Set M
a b : M
inst✝ : GroupWithZero M
ha : a ∈ centralizer S
h : a = 0
⊢ 0 ∈ centralizer S
M : Type u_1
S T : Set M
a b : M
inst✝ : GroupWithZero M
ha : a ∈ centralizer S
h : a = 0
⊢ a⁻¹ ∈ centralizer S
rw [h, inv_zero]
no goals
M : Type u_1
S T : Set M
a b : M
inst✝ : GroupWithZero M
ha : a ∈ centralizer S
h : a = 0
⊢ 0 ∈ centralizer S
exact zero_mem_centralizer S
no goals
M : Type u_1
S T : Set M
a b : M
inst✝ : GroupWithZero M
ha : a ∈ centralizer S
ha0 : a ≠ 0
c : M
hc : c ∈ S
⊢ c * a⁻¹ = a⁻¹ * c
rw [mul_inv_eq_iff_eq_mul₀ ha0, mul_assoc, eq_inv_mul_iff_mul_eq₀ ha0, ha c hc]