Documentation

Mathlib.GroupTheory.Subsemigroup.Centralizer

Centralizers of magmas and semigroups #

Main definitions #

We provide Monoid.centralizer, AddMonoid.centralizer, Subgroup.centralizer, and AddSubgroup.centralizer in other files.

def Set.addCentralizer {M : Type u_1} (S : Set M) [Add M] :
Set M

The centralizer of a subset of an additive magma.

Equations
Instances For
    def Set.centralizer {M : Type u_1} (S : Set M) [Mul M] :
    Set M

    The centralizer of a subset of a magma.

    Equations
    Instances For
      theorem Set.mem_addCentralizer {M : Type u_1} {S : Set M} [Add M] {c : M} :
      c Set.addCentralizer S mS, m + c = c + m
      theorem Set.mem_centralizer_iff {M : Type u_1} {S : Set M} [Mul M] {c : M} :
      c Set.centralizer S mS, m * c = c * m
      instance Set.decidableMemAddCentralizer {M : Type u_1} {S : Set M} [Add M] [(a : M) → Decidable (bS, b + a = a + b)] :
      Equations
      instance Set.decidableMemCentralizer {M : Type u_1} {S : Set M} [Mul M] [(a : M) → Decidable (bS, b * a = a * b)] :
      DecidablePred fun (x : M) => x Set.centralizer S
      Equations
      @[simp]
      theorem Set.one_mem_centralizer {M : Type u_1} (S : Set M) [MulOneClass M] :
      @[simp]
      @[simp]
      theorem Set.add_mem_addCentralizer {M : Type u_1} {S : Set M} {a : M} {b : M} [AddSemigroup M] (ha : a Set.addCentralizer S) (hb : b Set.addCentralizer S) :
      @[simp]
      theorem Set.mul_mem_centralizer {M : Type u_1} {S : Set M} {a : M} {b : M} [Semigroup M] (ha : a Set.centralizer S) (hb : b Set.centralizer S) :
      @[simp]
      theorem Set.neg_mem_addCentralizer {M : Type u_1} {S : Set M} {a : M} [AddGroup M] (ha : a Set.addCentralizer S) :
      @[simp]
      theorem Set.inv_mem_centralizer {M : Type u_1} {S : Set M} {a : M} [Group M] (ha : a Set.centralizer S) :
      @[simp]
      theorem Set.add_mem_centralizer {M : Type u_1} {S : Set M} {a : M} {b : M} [Distrib M] (ha : a Set.centralizer S) (hb : b Set.centralizer S) :
      @[simp]
      theorem Set.neg_mem_centralizer {M : Type u_1} {S : Set M} {a : M} [Mul M] [HasDistribNeg M] (ha : a Set.centralizer S) :
      @[simp]
      theorem Set.inv_mem_centralizer₀ {M : Type u_1} {S : Set M} {a : M} [GroupWithZero M] (ha : a Set.centralizer S) :
      @[simp]
      theorem Set.sub_mem_addCentralizer {M : Type u_1} {S : Set M} {a : M} {b : M} [AddGroup M] (ha : a Set.addCentralizer S) (hb : b Set.addCentralizer S) :
      @[simp]
      theorem Set.div_mem_centralizer {M : Type u_1} {S : Set M} {a : M} {b : M} [Group M] (ha : a Set.centralizer S) (hb : b Set.centralizer S) :
      @[simp]
      theorem Set.div_mem_centralizer₀ {M : Type u_1} {S : Set M} {a : M} {b : M} [GroupWithZero M] (ha : a Set.centralizer S) (hb : b Set.centralizer S) :
      theorem Set.addCentralizer_subset {M : Type u_1} {S : Set M} {T : Set M} [Add M] (h : S T) :
      theorem Set.centralizer_subset {M : Type u_1} {S : Set M} {T : Set M} [Mul M] (h : S T) :
      @[simp]
      theorem Set.centralizer_eq_top_iff_subset {M : Type u_1} {s : Set M} [Semigroup M] :
      @[simp]
      @[simp]
      theorem Set.addCentralizer_eq_univ {M : Type u_1} (S : Set M) [AddCommSemigroup M] :
      @[simp]
      theorem Set.centralizer_eq_univ {M : Type u_1} (S : Set M) [CommSemigroup M] :
      Set.centralizer S = Set.univ

      The centralizer of a subset of an additive semigroup.

      Equations
      Instances For

        The centralizer of a subset of a semigroup M.

        Equations
        Instances For
          theorem AddSubsemigroup.mem_centralizer_iff {M : Type u_1} {S : Set M} [AddSemigroup M] {z : M} :
          z AddSubsemigroup.centralizer S gS, g + z = z + g
          theorem Subsemigroup.mem_centralizer_iff {M : Type u_1} {S : Set M} [Semigroup M] {z : M} :
          z Subsemigroup.centralizer S gS, g * z = z * g
          instance AddSubsemigroup.decidableMemCentralizer {M : Type u_1} {S : Set M} [AddSemigroup M] (a : M) [Decidable (bS, b + a = a + b)] :
          Equations
          instance Subsemigroup.decidableMemCentralizer {M : Type u_1} {S : Set M} [Semigroup M] (a : M) [Decidable (bS, b * a = a * b)] :
          Equations