Documentation

Mathlib.GroupTheory.Submonoid.Center

Centers of monoids #

Main definitions #

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

def AddSubmonoid.center (M : Type u_1) [inst : AddMonoid M] :

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

Equations
  • One or more equations did not get rendered due to their size.
Equations
def AddSubmonoid.center.proof_1 (M : Type u_1) [inst : AddMonoid M] :
∀ {a b : M}, a Set.addCenter Mb Set.addCenter Ma + b Set.addCenter M
Equations
def Submonoid.center (M : Type u_1) [inst : Monoid M] :

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

Equations
  • One or more equations did not get rendered due to their size.
theorem Submonoid.coe_center (M : Type u_1) [inst : Monoid M] :
@[simp]
theorem Submonoid.center_toSubsemigroup (M : Type u_1) [inst : Monoid M] :
theorem AddSubmonoid.mem_center_iff {M : Type u_1} [inst : AddMonoid M] {z : M} :
z AddSubmonoid.center M ∀ (g : M), g + z = z + g
theorem Submonoid.mem_center_iff {M : Type u_1} [inst : Monoid M] {z : M} :
z Submonoid.center M ∀ (g : M), g * z = z * g
instance AddSubmonoid.decidableMemCenter {M : Type u_1} [inst : AddMonoid M] (a : M) [inst : Decidable (∀ (b : M), b + a = a + b)] :
Equations
instance Submonoid.decidableMemCenter {M : Type u_1} [inst : Monoid M] (a : M) [inst : Decidable (∀ (b : M), b * a = a * b)] :
Equations
instance Submonoid.center.commMonoid {M : Type u_1} [inst : Monoid M] :

The center of a monoid is commutative.

Equations
instance Submonoid.center.smulCommClass_left {M : Type u_1} [inst : Monoid M] :

The center of a monoid acts commutatively on that monoid.

Equations
instance Submonoid.center.smulCommClass_right {M : Type u_1} [inst : Monoid M] :

The center of a monoid acts commutatively on that monoid.

Equations

Note that smulCommClass (center M) (center M) M is already implied by Submonoid.smulCommClass_right

@[simp]