le_centralizer_centralizer — Mathlib

English

The elemental algebra generated by x is contained in the double centralizer of {x}: elemental R x ≤ centralizer R (centralizer R { x }).

Русский

Элементарная алгебра, порождаемая x, содержится в двойном центральизаторе множества {x}: elemental R x ≤ centralizer R (centralizer R { x }).

LaTeX

$$elemental(R,x) ≤ centralizer(R, centralizer(R\{x\}))$$

Lean4

theorem le_centralizer_centralizer [T2Space A] (x : A) : elemental R x ≤ centralizer R (centralizer R { x }) :=
  topologicalClosure_adjoin_le_centralizer_centralizer R { x }

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