# Centers of subgroups #

theorem AddSubgroup.center.proof_1 (G : Type u_1) [] :
∀ {a b : G}, a .carrierb .carriera + b .carrier
def AddSubgroup.center (G : Type u_1) [] :

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

Equations
• = { carrier := , add_mem' := , zero_mem' := , neg_mem' := }
Instances For
theorem AddSubgroup.center.proof_2 (G : Type u_1) [] :
0 .carrier
theorem AddSubgroup.center.proof_3 (G : Type u_1) [] :
∀ {x : G},
def Subgroup.center (G : Type u_1) [] :

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

Equations
• = { carrier := , mul_mem' := , one_mem' := , inv_mem' := }
Instances For
theorem AddSubgroup.coe_center (G : Type u_1) [] :
theorem Subgroup.coe_center (G : Type u_1) [] :
=
@[simp]
theorem AddSubgroup.center_toAddSubmonoid (G : Type u_1) [] :
@[simp]
theorem Subgroup.center_toSubmonoid (G : Type u_1) [] :
.toSubmonoid =
instance Subgroup.center.isCommutative (G : Type u_1) [] :
.IsCommutative
Equations
• =
@[simp]
theorem Subgroup.val_centerUnitsEquivUnitsCenter_apply_coe (G₀ : Type u_2) [] (a : { x : G₀ˣ // }) :
= a
@[simp]
theorem Subgroup.val_centerUnitsEquivUnitsCenter_symm_apply_coe (G₀ : Type u_2) [] (u : { x : G₀ // }ˣ) :
(.symm u) = u
def Subgroup.centerUnitsEquivUnitsCenter (G₀ : Type u_2) [] :
{ x : G₀ˣ // } ≃* { x : G₀ // }ˣ

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.
Instances For
theorem AddSubgroup.mem_center_iff {G : Type u_1} [] {z : G} :
∀ (g : G), g + z = z + g
theorem Subgroup.mem_center_iff {G : Type u_1} [] {z : G} :
∀ (g : G), g * z = z * g
instance Subgroup.decidableMemCenter {G : Type u_1} [] (z : G) [Decidable (∀ (g : G), g * z = z * g)] :
Equations
instance AddSubgroup.centerCharacteristic {G : Type u_1} [] :
.Characteristic
Equations
• =
instance Subgroup.centerCharacteristic {G : Type u_1} [] :
.Characteristic
Equations
• =
theorem CommGroup.center_eq_top {G : Type u_2} [] :
def Group.commGroupOfCenterEqTop {G : Type u_1} [] (h : ) :

A group is commutative if the center is the whole group

Equations
Instances For
theorem AddSubgroup.center_le_normalizer {G : Type u_1} [] {H : } :
H.normalizer
theorem Subgroup.center_le_normalizer {G : Type u_1} [] {H : } :
H.normalizer
theorem IsConj.eq_of_left_mem_center {M : Type u_2} [] {g : M} {h : M} (H : IsConj g h) (Hg : g ) :
g = h
theorem IsConj.eq_of_right_mem_center {M : Type u_2} [] {g : M} {h : M} (H : IsConj g h) (Hh : h ) :
g = h
theorem ConjClasses.mk_bijOn (G : Type u_2) [] :
Set.BijOn ConjClasses.mk (↑)