# mathlib3documentation

group_theory.subsemigroup.center

# Centers of magmas and semigroups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

## Main definitions #

• set.center: the center of a magma
• subsemigroup.center: the center of a semigroup
• set.add_center: the center of an additive magma
• add_subsemigroup.center: the center of an additive semigroup

We provide submonoid.center, add_submonoid.center, subgroup.center, add_subgroup.center, subsemiring.center, and subring.center in other files.

def set.center (M : Type u_1) [has_mul M] :
set M

The center of a magma.

Equations
• = {z : M | (m : M), m * z = z * m}
set M

The center of an additive magma.

Equations
• = {z : M | (m : M), m + z = z + m}
theorem set.mem_add_center (M : Type u_1) [has_add M] {z : M} :
(g : M), g + z = z + g
theorem set.mem_center_iff (M : Type u_1) [has_mul M] {z : M} :
z (g : M), g * z = z * g
@[protected, instance]
def set.decidable_mem_center (M : Type u_1) [has_mul M] [Π (a : M), decidable ( (b : M), b * a = a * b)] :
decidable_pred (λ (_x : M), _x set.center M)
Equations
@[simp]
theorem set.zero_mem_add_center (M : Type u_1)  :
@[simp]
theorem set.one_mem_center (M : Type u_1)  :
1
@[simp]
theorem set.zero_mem_center (M : Type u_1)  :
0
@[simp]
theorem set.mul_mem_center {M : Type u_1} [semigroup M] {a b : M} (ha : a ) (hb : b ) :
a * b
@[simp]
theorem set.add_mem_add_center {M : Type u_1} {a b : M} (ha : a ) (hb : b ) :
a + b
@[simp]
theorem set.inv_mem_center {M : Type u_1} [group M] {a : M} (ha : a ) :
@[simp]
theorem set.neg_mem_add_center {M : Type u_1} [add_group M] {a : M} (ha : a ) :
@[simp]
theorem set.add_mem_center {M : Type u_1} [distrib M] {a b : M} (ha : a ) (hb : b ) :
a + b
@[simp]
theorem set.neg_mem_center {M : Type u_1} [ring M] {a : M} (ha : a ) :
-a
theorem set.subset_center_units {M : Type u_1} [monoid M] :
theorem set.center_units_subset {M : Type u_1}  :
theorem set.center_units_eq {M : Type u_1}  :

In a group with zero, the center of the units is the preimage of the center.

@[simp]
theorem set.inv_mem_center₀ {M : Type u_1} {a : M} (ha : a ) :
@[simp]
theorem set.div_mem_center {M : Type u_1} [group M] {a b : M} (ha : a ) (hb : b ) :
a / b
@[simp]
theorem set.sub_mem_add_center {M : Type u_1} [add_group M] {a b : M} (ha : a ) (hb : b ) :
a - b
@[simp]
theorem set.div_mem_center₀ {M : Type u_1} {a b : M} (ha : a ) (hb : b ) :
a / b
@[simp]
theorem set.add_center_eq_univ (M : Type u_1)  :
@[simp]
theorem set.center_eq_univ (M : Type u_1)  :
def subsemigroup.center (M : Type u_1) [semigroup M] :

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

Equations
Instances for ↥subsemigroup.center
def add_subsemigroup.center (M : Type u_1)  :

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

Equations
Instances for ↥add_subsemigroup.center
theorem add_subsemigroup.coe_center (M : Type u_1)  :
theorem subsemigroup.coe_center (M : Type u_1) [semigroup M] :
theorem subsemigroup.mem_center_iff {M : Type u_1} [semigroup M] {z : M} :
(g : M), g * z = z * g
theorem add_subsemigroup.mem_center_iff {M : Type u_1} {z : M} :
(g : M), g + z = z + g
@[protected, instance]
def subsemigroup.decidable_mem_center {M : Type u_1} [semigroup M] (a : M) [decidable ( (b : M), b * a = a * b)] :
Equations
@[protected, instance]
def add_subsemigroup.decidable_mem_center {M : Type u_1} (a : M) [decidable ( (b : M), b + a = a + b)] :
Equations
@[protected, instance]

The center of an additive semigroup is commutative.

Equations
@[protected, instance]

The center of a semigroup is commutative.

Equations
@[simp]
theorem subsemigroup.center_eq_top (M : Type u_1)  :
@[simp]
theorem add_subsemigroup.center_eq_top (M : Type u_1)  :