Documentation

Mathlib.GroupTheory.Subsemigroup.Center

Centers of magmas and semigroups #

Main definitions #

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

def Set.addCenter (M : Type u_1) [inst : Add M] :
Set M

The center of an additive magma.

Equations
def Set.center (M : Type u_1) [inst : Mul M] :
Set M

The center of a magma.

Equations
theorem Set.mem_addCenter_iff (M : Type u_1) [inst : Add M] {z : M} :
z Set.addCenter M ∀ (g : M), g + z = z + g
theorem Set.mem_center_iff (M : Type u_1) [inst : Mul M] {z : M} :
z Set.center M ∀ (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)] :
Equations
@[simp]
theorem Set.zero_mem_addCenter (M : Type u_1) [inst : AddZeroClass M] :
@[simp]
theorem Set.one_mem_center (M : Type u_1) [inst : MulOneClass M] :
@[simp]
theorem Set.zero_mem_center (M : Type u_1) [inst : MulZeroClass M] :
@[simp]
theorem Set.add_mem_addCenter {M : Type u_1} [inst : AddSemigroup M] {a : M} {b : M} (ha : a Set.addCenter M) (hb : b Set.addCenter M) :
@[simp]
theorem Set.mul_mem_center {M : Type u_1} [inst : Semigroup M] {a : M} {b : M} (ha : a Set.center M) (hb : b Set.center M) :
@[simp]
theorem Set.neg_mem_addCenter {M : Type u_1} [inst : AddGroup M] {a : M} (ha : a Set.addCenter M) :
@[simp]
theorem Set.inv_mem_center {M : Type u_1} [inst : Group M] {a : M} (ha : a Set.center M) :
@[simp]
theorem Set.add_mem_center {M : Type u_1} [inst : Distrib M] {a : M} {b : M} (ha : a Set.center M) (hb : b Set.center M) :
@[simp]
theorem Set.neg_mem_center {M : Type u_1} [inst : Ring M] {a : M} (ha : a Set.center M) :
theorem Set.subset_center_units {M : Type u_1} [inst : Monoid M] :
theorem Set.center_units_eq {M : Type u_1} [inst : GroupWithZero M] :

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 : GroupWithZero M] {a : M} (ha : a Set.center M) :
@[simp]
theorem Set.sub_mem_addCenter {M : Type u_1} [inst : AddGroup M] {a : M} {b : M} (ha : a Set.addCenter M) (hb : b Set.addCenter M) :
@[simp]
theorem Set.div_mem_center {M : Type u_1} [inst : Group M] {a : M} {b : M} (ha : a Set.center M) (hb : b Set.center M) :
@[simp]
theorem Set.div_mem_center₀ {M : Type u_1} [inst : GroupWithZero M] {a : M} {b : M} (ha : a Set.center M) (hb : b Set.center M) :
@[simp]
theorem Set.addCenter_eq_univ (M : Type u_1) [inst : AddCommSemigroup M] :
Set.addCenter M = Set.univ
@[simp]
theorem Set.center_eq_univ (M : Type u_1) [inst : CommSemigroup M] :
Set.center M = Set.univ
def AddSubsemigroup.center.proof_1 (M : Type u_1) [inst : AddSemigroup M] :
∀ {a b : M}, a Set.addCenter Mb Set.addCenter Ma + b Set.addCenter M
Equations

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

Equations
def Subsemigroup.center (M : Type u_1) [inst : Semigroup M] :

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

Equations
theorem AddSubsemigroup.mem_center_iff {M : Type u_1} [inst : AddSemigroup M] {z : M} :
z AddSubsemigroup.center M ∀ (g : M), g + z = z + g
theorem Subsemigroup.mem_center_iff {M : Type u_1} [inst : Semigroup M] {z : M} :
z Subsemigroup.center M ∀ (g : M), g * z = z * g
instance AddSubsemigroup.decidableMemCenter {M : Type u_1} [inst : AddSemigroup M] (a : M) [inst : Decidable (∀ (b : M), b + a = a + b)] :
Equations
instance Subsemigroup.decidableMemCenter {M : Type u_1} [inst : Semigroup M] (a : M) [inst : Decidable (∀ (b : M), b * a = a * b)] :
Equations
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.