mem_centralizer_iff

Mathlib.Algebra.Ring.Subring.Basic

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

English

z ∈ centralizer s iff ∀ g ∈ s, g z = z g

Русский

z принадлежит центральлизатору множества s тогда и только тогда, когда для всех g ∈ s выполняется g z = z g

LaTeX

$$z ∈ centralizer s ↔ ∀ g ∈ s, g z = z g$$

Lean4

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

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

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

Разделы

Аффилиация

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