commute_of_mem_adjoin_singleton_of_commute

Mathlib.Algebra.Algebra.NonUnitalSubalgebra

URI: https://scilib.ai/kg/mathlib#NonUnitalAlgebra.commute_of_mem_adjoin_singleton_of_commute

← MathLib Explorer

English

If c ∈ adjoin R { b } and a commutes with b, then a commutes with c.

Русский

Если c ∈ adjoin R { b } и a коммутирует с b, то a коммутирует с c.

LaTeX

$$hb: c ∈ adjoin(R,{b}) and h: Commute a b implies Commute a c$$

Lean4

theorem commute_of_mem_adjoin_singleton_of_commute {a b c : A} (hc : c ∈ adjoin R { b }) (h : Commute a b) :
    Commute a c :=
  commute_of_mem_adjoin_of_forall_mem_commute hc <| by simpa

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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