Documentation

Mathlib.Algebra.GroupWithZero.Center

Center of a group with zero #

@[simp]
theorem Set.zero_mem_center {M₀ : Type u_1} [MulZeroClass 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₀] :
Set.center G₀ˣ Units.val ⁻¹' Set.center G₀
theorem Set.center_units_eq {G₀ : Type u_2} [GroupWithZero G₀] :
Set.center G₀ˣ = Units.val ⁻¹' Set.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 : G₀} {b : G₀} (ha : a s.centralizer) (hb : b s.centralizer) :
a / b s.centralizer
@[deprecated Set.inv_mem_center]
theorem Set.inv_mem_center₀ {G₀ : Type u_2} [GroupWithZero G₀] {a : G₀} (ha : a Set.center G₀) :
@[deprecated Set.div_mem_center]
theorem Set.div_mem_center₀ {G₀ : Type u_2} [GroupWithZero G₀] {a : G₀} {b : G₀} (ha : a Set.center G₀) (hb : b Set.center G₀) :
a / b Set.center G₀