mem_centralizer_iff

Mathlib.Algebra.Algebra.NonUnitalSubalgebra

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

English

An element z lies in centralizer(R,s) iff z commutes with every element of s.

Русский

Элемент z принадлежит centralizer(R,s) тогда и только тогда, когда z коммутирует с каждым элементом s.

LaTeX

$$z ∈ centralizer(R,s) ↔ ∀ g ∈ s, gz = zg$$

Lean4

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

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

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

Разделы

Аффилиация

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