Documentation

Mathlib.GroupTheory.Submonoid.Centralizer

Centralizers of magmas and monoids #

Main definitions #

We provide Subgroup.centralizer, AddSubgroup.centralizer in other files.

def Submonoid.centralizer {M : Type u_1} (S : Set M) [Monoid M] :

The centralizer of a subset of a monoid M.

Equations
    Instances For

      The centralizer of a subset of an additive monoid.

      Equations
        Instances For
          @[simp]
          theorem Submonoid.coe_centralizer {M : Type u_1} (S : Set M) [Monoid M] :
          @[simp]
          theorem Submonoid.mem_centralizer_iff {M : Type u_1} {S : Set M} [Monoid M] {z : M} :
          z centralizer S gS, g * z = z * g
          theorem AddSubmonoid.mem_centralizer_iff {M : Type u_1} {S : Set M} [AddMonoid M] {z : M} :
          z centralizer S gS, g + z = z + g
          instance Submonoid.decidableMemCentralizer {M : Type u_1} {S : Set M} [Monoid M] (a : M) [Decidable (∀ bS, b * a = a * b)] :
          Equations
            instance AddSubmonoid.decidableMemCentralizer {M : Type u_1} {S : Set M} [AddMonoid M] (a : M) [Decidable (∀ bS, b + a = a + b)] :
            Equations
              theorem Submonoid.centralizer_le {M : Type u_1} {S T : Set M} [Monoid M] (h : S T) :
              theorem AddSubmonoid.centralizer_le {M : Type u_1} {S T : Set M} [AddMonoid M] (h : S T) :
              @[simp]
              @[reducible, inline]
              abbrev Submonoid.closureCommMonoidOfComm (M : Type u_1) [Monoid M] {s : Set M} (hcomm : as, bs, a * b = b * a) :

              If all the elements of a set s commute, then closure s is a commutative monoid.

              Equations
                Instances For
                  @[reducible, inline]
                  abbrev AddSubmonoid.closureAddCommMonoidOfComm (M : Type u_1) [AddMonoid M] {s : Set M} (hcomm : as, bs, a + b = b + a) :

                  If all the elements of a set s commute, then closure s forms an additive commutative monoid.

                  Equations
                    Instances For