center_le_centralizer — Mathlib

English

Let R be a nonunital semiring. For every subset s of R, every element of the center of R commutes with every element of s; equivalently, center(R) ⊆ centralizer(s).

Русский

Пусть R — несуществующее единичное полускольцо (nonunital semiring). Для любого множества s ⊆ R каждый элемент центра R коммутирует с любым элементом s; то есть Z(R) ⊆ C_R(s).

LaTeX

$$$\operatorname{center}(R) \le \operatorname{centralizer}(s)$$$

Lean4

theorem center_le_centralizer {R} [NonUnitalSemiring R] (s) : center R ≤ centralizer s :=
  s.center_subset_centralizer

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