Center of a group with zero

@[simp]

theorem Set.zero_mem_center {M₀ : Type u_1} [MulZeroClass M₀] : 0 ∈ center M₀

@[simp]

theorem Set.zero_mem_centralizer {M₀ : Type u_1} [MulZeroClass M₀] {s : Set M₀} : 0 ∈ s.centralizer

theorem Set.center_units_subset {G₀ : Type u_2} [GroupWithZero G₀] : center G₀ˣ ⊆ Units.val ⁻¹' center G₀

theorem Set.center_units_eq {G₀ : Type u_2} [GroupWithZero G₀] : center G₀ˣ = Units.val ⁻¹' center G₀

In a group with zero, the center of the units is the preimage of the center.

@[simp]

theorem Set.inv_mem_centralizer₀ {G₀ : Type u_2} [GroupWithZero G₀] {s : Set G₀} {a : G₀} (ha : a ∈ s.centralizer) : a⁻¹ ∈ s.centralizer

@[simp]

theorem Set.div_mem_centralizer₀ {G₀ : Type u_2} [GroupWithZero G₀] {s : Set G₀} {a b : G₀} (ha : a ∈ s.centralizer) (hb : b ∈ s.centralizer) : a / b ∈ s.centralizer