centralizer_eq_top_iff_subset — Mathlib

English

The centralizer of S equals the top submonoid ⊤ if and only if S is contained in the center of M.

Русский

Централизатор S равен верхнему подмножеству ⊤ тогда и только тогда, когда S ⊆ Z(M).

LaTeX

$$$ \operatorname{centralizer}(S) = \top \iff S \subseteq \operatorname{center}(M) $$$

Lean4

@[to_additive (attr := simp)]
theorem centralizer_eq_top_iff_subset {s : Set M} : centralizer s = ⊤ ↔ s ⊆ center M :=
  SetLike.ext'_iff.trans Set.centralizer_eq_top_iff_subset

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