mem_centralizer_iff

Mathlib.Algebra.Algebra.Subalgebra.Basic

URI: https://scilib.ai/kg/mathlib#Subalgebra.mem_centralizer_iff

English

Any subalgebra s is contained in the centralizer of the centralizer of s.

Русский

Любая подалгебра s содержится в центральизаторе центральизатора s.

LaTeX

$$$s \le \text{centralizer}(R, \text{centralizer}(R, (s : \text{Set} A)))$$$

Lean4

theorem mem_centralizer_iff {s : Set A} {z : A} : z ∈ centralizer R s ↔ ∀ g ∈ s, g * z = z * g :=
  Iff.rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru