Subsemigroup.mem_center_iff

theorem Subsemigroup.mem_center_iff : ∀ {M : Type u_1} [inst : Semigroup M] {z : M}, z ∈ Subsemigroup.center M ↔ ∀ (g : M), g * z = z * g

The theorem `Subsemigroup.mem_center_iff` states for any type `M` that forms a semigroup under an operation, an element `z` from `M` belongs to the center of the semigroup if and only if it commutes with every other element `g` from `M`. In other words, `z` is in the center of the semigroup if for all `g` in `M`, the operation of `g` with `z` results in the same as the operation of `z` with `g`.

More concisely: An element belongs to the center of a semigroup if and only if it commutes with every other element in the semigroup.