Subgroup.mem_center_iff

theorem Subgroup.mem_center_iff : ∀ {G : Type u_1} [inst : Group G] {z : G}, z ∈ Subgroup.center G ↔ ∀ (g : G), g * z = z * g

The theorem `Subgroup.mem_center_iff` states that for any group `G` and any element `z` in `G`, `z` is in the center of the group `G` if and only if `z` commutes with every element `g` in `G`. In other words, for all `g` in `G`, the product of `g` and `z` equals the product of `z` and `g`. This theorem provides a characterization of the center of a group in terms of commutativity.

More concisely: A group element is in the center if and only if it commutes with every group element.