div_right

Mathlib.Algebra.GroupWithZero.Commute

URI: https://scilib.ai/kg/mathlib#Commute.div_right

English

If a commutes with b and with c, then a commutes with b/c.

Русский

Если a коммутирует с b и с c, то a коммутирует с b/c.

LaTeX

$$$Commute a b \land Commute a c \Rightarrow Commute a (b / c)$$$

Lean4

@[simp]
theorem div_right (hab : Commute a b) (hac : Commute a c) : Commute a (b / c) :=
  SemiconjBy.div_right hab hac

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

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

Разделы

Аффилиация

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