commute_of_mem_adjoin_singleton_of_commute

Mathlib.Algebra.Algebra.Subalgebra.Lattice

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

← MathLib Explorer

English

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

Русский

Если b ∈ adjoin_R{a}, то a commute с b.

LaTeX

$$$\\text{If } b \\in \\operatorname{adjoin}_R\\{a\\}, \\ \\operatorname{Commute}(a,b)$$$

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