[GOAL]
M : Type u_1
inst✝ : MulOneClass M
⊢ 1 ∈ center M
[PROOFSTEP]
simp [mem_center_iff]
[GOAL]
M : Type u_1
inst✝ : MulZeroClass M
⊢ 0 ∈ center M
[PROOFSTEP]
simp [mem_center_iff]
[GOAL]
M : Type u_1
inst✝ : Semigroup M
a b : M
ha : a ∈ center M
hb : b ∈ center M
g : M
⊢ g * (a * b) = a * b * g
[PROOFSTEP]
rw [mul_assoc, ← hb g, ← mul_assoc, ha g, mul_assoc]
[GOAL]
M : Type u_1
inst✝ : Group M
a : M
ha : a ∈ center M
g : M
⊢ g * a⁻¹ = a⁻¹ * g
[PROOFSTEP]
rw [← inv_inj, mul_inv_rev, inv_inv, ← ha, mul_inv_rev, inv_inv]
[GOAL]
M : Type u_1
inst✝ : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
c : M
⊢ c * (a + b) = (a + b) * c
[PROOFSTEP]
rw [add_mul, mul_add, ha c, hb c]
[GOAL]
M : Type u_1
inst✝ : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
c : M
⊢ c * -a = -a * c
[PROOFSTEP]
rw [← neg_mul_comm, ha (-c), neg_mul_comm]
[GOAL]
M : Type u_1
inst✝ : GroupWithZero M
a : Mˣ
ha : a ∈ center Mˣ
b : M
⊢ b * ↑a = ↑a * b
[PROOFSTEP]
obtain rfl | hb := eq_or_ne b 0
[GOAL]
case inl
M : Type u_1
inst✝ : GroupWithZero M
a : Mˣ
ha : a ∈ center Mˣ
⊢ 0 * ↑a = ↑a * 0
[PROOFSTEP]
rw [zero_mul, mul_zero]
[GOAL]
case inr
M : Type u_1
inst✝ : GroupWithZero M
a : Mˣ
ha : a ∈ center Mˣ
b : M
hb : b ≠ 0
⊢ b * ↑a = ↑a * b
[PROOFSTEP]
exact Units.ext_iff.mp (ha (Units.mk0 _ hb))
[GOAL]
M : Type u_1
inst✝ : GroupWithZero M
a : M
ha : a ∈ center M
⊢ a⁻¹ ∈ center M
[PROOFSTEP]
obtain rfl | ha0 := eq_or_ne a 0
[GOAL]
case inl
M : Type u_1
inst✝ : GroupWithZero M
ha : 0 ∈ center M
⊢ 0⁻¹ ∈ center M
[PROOFSTEP]
rw [inv_zero]
[GOAL]
case inl
M : Type u_1
inst✝ : GroupWithZero M
ha : 0 ∈ center M
⊢ 0 ∈ center M
[PROOFSTEP]
exact zero_mem_center M
[GOAL]
case inr
M : Type u_1
inst✝ : GroupWithZero M
a : M
ha : a ∈ center M
ha0 : a ≠ 0
⊢ a⁻¹ ∈ center M
[PROOFSTEP]
rcases IsUnit.mk0 _ ha0 with ⟨a, rfl⟩
[GOAL]
case inr.intro
M : Type u_1
inst✝ : GroupWithZero M
a : Mˣ
ha : ↑a ∈ center M
ha0 : ↑a ≠ 0
⊢ (↑a)⁻¹ ∈ center M
[PROOFSTEP]
rw [← Units.val_inv_eq_inv_val]
[GOAL]
case inr.intro
M : Type u_1
inst✝ : GroupWithZero M
a : Mˣ
ha : ↑a ∈ center M
ha0 : ↑a ≠ 0
⊢ ↑a⁻¹ ∈ center M
[PROOFSTEP]
exact center_units_subset (inv_mem_center (subset_center_units ha))
[GOAL]
M : Type u_1
inst✝ : Group M
a b : M
ha : a ∈ center M
hb : b ∈ center M
⊢ a / b ∈ center M
[PROOFSTEP]
rw [div_eq_mul_inv]
[GOAL]
M : Type u_1
inst✝ : Group M
a b : M
ha : a ∈ center M
hb : b ∈ center M
⊢ a * b⁻¹ ∈ center M
[PROOFSTEP]
exact mul_mem_center ha (inv_mem_center hb)
[GOAL]
M : Type u_1
inst✝ : GroupWithZero M
a b : M
ha : a ∈ center M
hb : b ∈ center M
⊢ a / b ∈ center M
[PROOFSTEP]
rw [div_eq_mul_inv]
[GOAL]
M : Type u_1
inst✝ : GroupWithZero M
a b : M
ha : a ∈ center M
hb : b ∈ center M
⊢ a * b⁻¹ ∈ center M
[PROOFSTEP]
exact mul_mem_center ha (inv_mem_center₀ hb)
