Documentation

Mathlib.GroupTheory.Subgroup.Center

Centers of subgroups #

The center of an additive group G is the set of elements that commute with everything in G

Equations
def Subgroup.center (G : Type u_1) [Group G] :

The center of a group G is the set of elements that commute with everything in G

Equations
@[simp]
theorem Subgroup.center_toSubmonoid (G : Type u_1) [Group G] :
instance Subgroup.center.isCommutative (G : Type u_1) [Group G] :
(Subgroup.center G).IsCommutative
Equations
  • =
@[simp]

For a group with zero, the center of the units is the same as the units of the center.

Equations
  • One or more equations did not get rendered due to their size.
theorem AddSubgroup.mem_center_iff {G : Type u_1} [AddGroup G] {z : G} :
z AddSubgroup.center G ∀ (g : G), g + z = z + g
theorem Subgroup.mem_center_iff {G : Type u_1} [Group G] {z : G} :
z Subgroup.center G ∀ (g : G), g * z = z * g
instance Subgroup.decidableMemCenter {G : Type u_1} [Group G] (z : G) [Decidable (∀ (g : G), g * z = z * g)] :
Equations
instance AddSubgroup.centerCharacteristic {G : Type u_1} [AddGroup G] :
(AddSubgroup.center G).Characteristic
Equations
  • =
instance Subgroup.centerCharacteristic {G : Type u_1} [Group G] :
(Subgroup.center G).Characteristic
Equations
  • =

A group is commutative if the center is the whole group

Equations
theorem Subgroup.center_le_normalizer {G : Type u_1} [Group G] {H : Subgroup G} :
Subgroup.center G H.normalizer
theorem IsConj.eq_of_left_mem_center {M : Type u_2} [Monoid M] {g : M} {h : M} (H : IsConj g h) (Hg : g Set.center M) :
g = h
theorem IsConj.eq_of_right_mem_center {M : Type u_2} [Monoid M] {g : M} {h : M} (H : IsConj g h) (Hh : h Set.center M) :
g = h
theorem ConjClasses.mk_bijOn (G : Type u_2) [Group G] :