Documentation

Mathlib.Algebra.GroupWithZero.Center

Center of a group with zero #

source
@[simp]
theorem Set.zero_mem_center {M₀ : Type u_1} [MulZeroClass M₀] :
0 ∈ center M₀
source
@[simp]
theorem Set.zero_mem_centralizer {M₀ : Type u_1} [MulZeroClass M₀] {s : Set M₀} :
0 ∈ s.centralizer
source
theorem Set.center_units_subset {G₀ : Type u_2} [GroupWithZero G₀] :
center G₀ˣ ⊆ Units.val ⁻¹' center G₀
source
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.

source
@[simp]
theorem Set.inv_mem_centralizer₀ {G₀ : Type u_2} [GroupWithZero G₀] {s : Set G₀} {a : G₀} (ha : a ∈ s.centralizer) :
a⁻¹ ∈ s.centralizer
source
@[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
source
@[deprecated Set.inv_mem_center (since := "2024-06-17")]
theorem Set.inv_mem_center₀ {G₀ : Type u_2} [GroupWithZero G₀] {a : G₀} (ha : a ∈ center G₀) :
a⁻¹ ∈ center G₀
source
@[deprecated Set.div_mem_center (since := "2024-06-17")]
theorem Set.div_mem_center₀ {G₀ : Type u_2} [GroupWithZero G₀] {a b : G₀} (ha : a ∈ center G₀) (hb : b ∈ center G₀) :
a / b ∈ center G₀