centralizer_eq_top_iff_subset — Mathlib

English

Let R be a semiring and s a subset of R. The set of elements that commute with every element of s is the whole ring if and only if every element of s commutes with every element of R; that is, centralizer(s) = ⊤ if and only if s ⊆ center(R).

Русский

Пусть R — полускольное кольцо, и s ⊆ R. Множество элементов, коммутирующих с каждым элементом из s, равно всему кольцу тогда и только тогда, когда каждый элемент из s коммутирует со всеми элементами кольца; то есть centralizer(s) = ⊤ тогда и только тогда, когда s ⊆ center(R).

LaTeX

$$$\\operatorname{centralizer}(s) = \\top \\iff s \\subseteq \\operatorname{center}(R)$$$

Lean4

@[simp]
theorem centralizer_eq_top_iff_subset {R} [Semiring R] {s : Set R} : centralizer s = ⊤ ↔ s ⊆ center R :=
  SetLike.ext'_iff.trans Set.centralizer_eq_top_iff_subset

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