mem_center_iff

Mathlib.Algebra.Algebra.NonUnitalSubalgebra

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

English

If r ∈ R and a ∈ Set.center A, then r•a ∈ Set.center A, i.e., scalar multiples preserve centrality.

Русский

Если r ∈ R и a ∈ центр A, тогда r•a ∈ центр A, то есть скалярные кратности сохраняют центральность.

LaTeX

$$r • a ∈ Set.center A$$

Lean4

theorem mem_center_iff {a : A} : a ∈ center R A ↔ ∀ b : A, b * a = a * b :=
  Subsemigroup.mem_center_iff

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

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

Разделы

Аффилиация

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