Center of a group with zero #
@[simp]
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)
:
@[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)
:
@[deprecated Set.inv_mem_center]
theorem
Set.inv_mem_center₀
{G₀ : Type u_2}
[GroupWithZero G₀]
{a : G₀}
(ha : a ∈ Set.center G₀)
:
a⁻¹ ∈ Set.center G₀
@[deprecated Set.div_mem_center]
theorem
Set.div_mem_center₀
{G₀ : Type u_2}
[GroupWithZero G₀]
{a b : G₀}
(ha : a ∈ Set.center G₀)
(hb : b ∈ Set.center G₀)
:
a / b ∈ Set.center G₀