center_subset_centralizer — Mathlib

English

The center of M is contained in the centralizer of any subset S of M; elements of the center commute with every element of S.

Русский

Центр M содержится во всём центральизаторе любой подмножества S множества M; элементы центра коммутируют с любым элементом S.

LaTeX

$$$ \mathrm{center}(M) \subseteq \mathrm{centralizer}(S). $$$

Lean4

@[to_additive addCenter_subset_addCentralizer]
theorem center_subset_centralizer (S : Set M) : Set.center M ⊆ S.centralizer := fun _ hx m _ ↦ (hx.comm m).symm

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