# Documentation

Mathlib.GroupTheory.Subsemigroup.Center

# Centers of magmas and semigroups #

## Main definitions #

• Set.center: the center of a magma
• Subsemigroup.center: the center of a semigroup
• Set.addCenter: the center of an additive magma
• AddSubsemigroup.center: the center of an additive semigroup

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

Set M

The center of an additive magma.

Equations
• = { z | ∀ (m : M), m + z = z + m }
def Set.center (M : Type u_1) [inst : Mul M] :
Set M

The center of a magma.

Equations
• = { z | ∀ (m : M), m * z = z * m }
theorem Set.mem_addCenter_iff (M : Type u_1) [inst : Add M] {z : M} :
∀ (g : M), g + z = z + g
theorem Set.mem_center_iff (M : Type u_1) [inst : Mul M] {z : M} :
z ∀ (g : M), g * z = z * g
instance Set.decidableMemCenter (M : Type u_1) [inst : Mul M] [inst : (a : M) → Decidable (∀ (b : M), b * a = a * b)] :
DecidablePred fun x => x
Equations
@[simp]
theorem Set.zero_mem_addCenter (M : Type u_1) [inst : ] :
@[simp]
theorem Set.one_mem_center (M : Type u_1) [inst : ] :
1
@[simp]
theorem Set.zero_mem_center (M : Type u_1) [inst : ] :
0
@[simp]
theorem Set.add_mem_addCenter {M : Type u_1} [inst : ] {a : M} {b : M} (ha : ) (hb : ) :
a + b
@[simp]
theorem Set.mul_mem_center {M : Type u_1} [inst : ] {a : M} {b : M} (ha : a ) (hb : b ) :
a * b
@[simp]
theorem Set.neg_mem_addCenter {M : Type u_1} [inst : ] {a : M} (ha : ) :
@[simp]
theorem Set.inv_mem_center {M : Type u_1} [inst : ] {a : M} (ha : a ) :
@[simp]
theorem Set.add_mem_center {M : Type u_1} [inst : ] {a : M} {b : M} (ha : a ) (hb : b ) :
a + b
@[simp]
theorem Set.neg_mem_center {M : Type u_1} [inst : Ring M] {a : M} (ha : a ) :
-a
theorem Set.subset_center_units {M : Type u_1} [inst : ] :
Units.val ⁻¹'
theorem Set.center_units_subset {M : Type u_1} [inst : ] :
Units.val ⁻¹'
theorem Set.center_units_eq {M : Type u_1} [inst : ] :
= Units.val ⁻¹'

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} [inst : ] {a : M} (ha : a ) :
@[simp]
theorem Set.sub_mem_addCenter {M : Type u_1} [inst : ] {a : M} {b : M} (ha : ) (hb : ) :
a - b
@[simp]
theorem Set.div_mem_center {M : Type u_1} [inst : ] {a : M} {b : M} (ha : a ) (hb : b ) :
a / b
@[simp]
theorem Set.div_mem_center₀ {M : Type u_1} [inst : ] {a : M} {b : M} (ha : a ) (hb : b ) :
a / b
@[simp]
theorem Set.addCenter_eq_univ (M : Type u_1) [inst : ] :
= Set.univ
@[simp]
theorem Set.center_eq_univ (M : Type u_1) [inst : ] :
= Set.univ
def AddSubsemigroup.center.proof_1 (M : Type u_1) [inst : ] :
∀ {a b : M}, a + b
Equations
• (_ : a + b ) = (_ : a + b )
def AddSubsemigroup.center (M : Type u_1) [inst : ] :

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

Equations
• = { carrier := , add_mem' := (_ : ∀ {a b : M}, a + b ) }
def Subsemigroup.center (M : Type u_1) [inst : ] :

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

Equations
• = { carrier := , mul_mem' := (_ : ∀ {a b : M}, a b a * b ) }
theorem AddSubsemigroup.mem_center_iff {M : Type u_1} [inst : ] {z : M} :
∀ (g : M), g + z = z + g
theorem Subsemigroup.mem_center_iff {M : Type u_1} [inst : ] {z : M} :
∀ (g : M), g * z = z * g
instance AddSubsemigroup.decidableMemCenter {M : Type u_1} [inst : ] (a : M) [inst : Decidable (∀ (b : M), b + a = a + b)] :
Equations
instance Subsemigroup.decidableMemCenter {M : Type u_1} [inst : ] (a : M) [inst : Decidable (∀ (b : M), b * a = a * b)] :
Equations
def AddSubsemigroup.instAddCommSemigroupSubtypeMemSubsemigroupToAddInstMembershipInstSetLikeSubsemigroupCenter.proof_2 {M : Type u_1} [inst : ] (a : { x // }) (b : { x // }) (c : { x // }) :
a + b + c = a + (b + c)
Equations
• (_ : ∀ (a b c : { x // }), a + b + c = a + (b + c)) = (_ : ∀ (a b c : { x // }), a + b + c = a + (b + c))
Equations
• (_ : x + b = b + x) = (_ : x + b = b + x)
Equations
• (_ : ) = (_ : )

The center of an additive semigroup is commutative.

Equations
• One or more equations did not get rendered due to their size.

The center of a semigroup is commutative.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem AddSubsemigroup.center_eq_top (M : Type u_1) [inst : ] :
@[simp]
theorem Subsemigroup.center_eq_top (M : Type u_1) [inst : ] :