center_eq_univ — Mathlib

English

In a commutative semigroup, every element commutes with every element, so the center is all of M.

Русский

В коммутативной полугруппе каждый элемент коммутирует с любым элементом, поэтому центр есть всё M.

LaTeX

$$$ \mathrm{center}(M) = \mathrm{univ}$ when M is commutative$$

Lean4

@[to_additive (attr := simp) addCenter_eq_univ]
theorem center_eq_univ : center M = univ :=
  (Subset.antisymm (subset_univ _)) fun _ _ => Semigroup.mem_center_iff.mpr (fun _ => mul_comm _ _)

Похожие утверждения