mem_center_iff — Mathlib

English

In a semigroup, z ∈ center M if and only if z commutes with every element g of M, i.e., ∀ g, g z = z g.

Русский

В полугруппе z ∈ центр M тогда и только тогда, когда он коммутирует с каждым элементом g из M, то есть ∀ g, g z = z g.

LaTeX

$$$ z \in \mathrm{center}(M) \iff \forall g,\; g z = z g $$$

Lean4

@[to_additive]
theorem _root_.Semigroup.mem_center_iff {z : M} : z ∈ Set.center M ↔ ∀ g, g * z = z * g :=
  ⟨fun a g ↦ by rw [IsMulCentral.comm a g], fun h ↦
    ⟨fun _ ↦ (h _).symm, fun _ _ ↦ (mul_assoc z _ _).symm, fun _ _ ↦ mul_assoc _ _ z⟩⟩

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