right_comm

Mathlib.Algebra.Group.Commute.Defs

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

English

If b and c commute, then a*b*c = a*c*b for any a.

Русский

Если b и c коммутируют, то a*b*c = a*c*b для любого a.

LaTeX

$$$\\forall S [Semigroup S],\\ \\forall b,c \\in S,\\ Commute b c \\rightarrow \\forall a \\in S,\\ a b c = a c b$$$

Lean4

@[to_additive]
protected theorem right_comm (h : Commute b c) (a : S) : a * b * c = a * c * b := by simp only [mul_assoc, h.eq]

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

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

Разделы

Аффилиация

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