Documentation

Mathlib.GroupTheory.Subgroup.Center

Centers of subgroups #

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

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

Equations
Instances For
    theorem AddSubgroup.center.proof_3 (G : Type u_1) [AddGroup G] :
    ∀ {x : G}, x Set.addCenter G-x Set.addCenter G
    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
    Instances For
      @[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.
      Instances For
        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
        Instances For
          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] :