mathlib documentation

group_theory.submonoid.center

Centers of magmas and monoids #

Main definitions #

We provide 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
def set.add_center (M : Type u_1) [has_add M] :
set M

The center of an additive magma.

Equations
theorem set.mem_add_center (M : Type u_1) [has_add M] {z : M} :
z set.add_center M ∀ (g : M), g + z = z + g
theorem set.mem_center_iff (M : Type u_1) [has_mul M] {z : M} :
z set.center M ∀ (g : M), g * z = z * g
@[instance]
def set.decidable_mem_center (M : Type u_1) [has_mul M] [decidable_eq M] [fintype M] :
decidable_pred (λ (_x : M), _x set.center M)
Equations
@[simp]
theorem set.zero_mem_add_center (M : Type u_1) [add_zero_class M] :
@[simp]
theorem set.one_mem_center (M : Type u_1) [mul_one_class M] :
@[simp]
theorem set.zero_mem_center (M : Type u_1) [mul_zero_class M] :
@[simp]
theorem set.mul_mem_center {M : Type u_1} [semigroup M] {a b : M} (ha : a set.center M) (hb : b set.center M) :
@[simp]
theorem set.add_mem_add_center {M : Type u_1} [add_semigroup M] {a b : M} (ha : a set.add_center M) (hb : b set.add_center M) :
@[simp]
theorem set.inv_mem_center {M : Type u_1} [group M] {a : M} (ha : a set.center M) :
@[simp]
theorem set.neg_mem_add_center {M : Type u_1} [add_group M] {a : M} (ha : a set.add_center M) :
@[simp]
theorem set.add_mem_center {M : Type u_1} [distrib M] {a b : M} (ha : a set.center M) (hb : b set.center M) :
@[simp]
theorem set.neg_mem_center {M : Type u_1} [ring M] {a : M} (ha : a set.center 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} [group_with_zero M] {a : M} (ha : a set.center M) :
@[simp]
theorem set.div_mem_center {M : Type u_1} [group M] {a b : M} (ha : a set.center M) (hb : b set.center M) :
@[simp]
theorem set.sub_mem_add_center {M : Type u_1} [add_group M] {a b : M} (ha : a set.add_center M) (hb : b set.add_center M) :
@[simp]
theorem set.div_mem_center₀ {M : Type u_1} [group_with_zero M] {a b : M} (ha : a set.center M) (hb : b set.center M) :
@[simp]
@[simp]
theorem set.center_eq_univ (M : Type u_1) [comm_semigroup M] :
def submonoid.center (M : Type u_1) [monoid M] :

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

Equations
def add_submonoid.center (M : Type u_1) [add_monoid M] :

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

Equations
theorem submonoid.coe_center (M : Type u_1) [monoid M] :
theorem add_submonoid.mem_center_iff {M : Type u_1} [add_monoid M] {z : M} :
z add_submonoid.center M ∀ (g : M), g + z = z + g
theorem submonoid.mem_center_iff {M : Type u_1} [monoid M] {z : M} :
z submonoid.center M ∀ (g : M), g * z = z * g
@[instance]
def submonoid.decidable_mem_center {M : Type u_1} [monoid M] [decidable_eq M] [fintype M] :
decidable_pred (λ (_x : M), _x submonoid.center M)
Equations
@[instance]

The center of a monoid is commutative.

Equations
@[simp]
theorem submonoid.center_eq_top (M : Type u_1) [comm_monoid M] :