Documentation

Mathlib.GroupTheory.Subsemigroup.Center

Centers of semigroups, as subsemigroups. #

Main definitions #

We provide Submonoid.center, AddSubmonoid.center, Subgroup.center, AddSubgroup.center, Subsemiring.center, and Subring.center in other files.

References #

Set.center as a Subsemigroup. #

The center of a semigroup M is the set of elements that commute with everything in M

Equations
Instances For

    The center of a semigroup M is the set of elements that commute with everything in M

    Equations
    Instances For
      theorem AddSubsemigroup.center.addCommSemigroup.proof_2 {M : Type u_1} [Add M] (a : { x : M // x AddSubsemigroup.center M }) :
      ∀ (x : { x : M // x AddSubsemigroup.center M }), a + x = x + a
      theorem AddSubsemigroup.center.addCommSemigroup.proof_1 {M : Type u_1} [Add M] :
      ∀ (x b x_1 : { x : M // x AddSubsemigroup.center M }), x + b + x_1 = x + (b + x_1)

      The center of an additive magma is commutative and associative.

      Equations

      The center of a magma is commutative and associative.

      Equations
      theorem AddSubsemigroup.mem_center_iff {M : Type u_1} [AddSemigroup M] {z : M} :
      z AddSubsemigroup.center M ∀ (g : M), g + z = z + g
      theorem Subsemigroup.mem_center_iff {M : Type u_1} [Semigroup M] {z : M} :
      z Subsemigroup.center M ∀ (g : M), g * z = z * g
      instance AddSubsemigroup.decidableMemCenter {M : Type u_1} [AddSemigroup M] (a : M) [Decidable (∀ (b : M), b + a = a + b)] :
      Equations
      instance Subsemigroup.decidableMemCenter {M : Type u_1} [Semigroup M] (a : M) [Decidable (∀ (b : M), b * a = a * b)] :
      Equations