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
    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] :

      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

        A group is commutative if the center is the whole group

        Equations
        Instances For
          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] :