left_comm

Mathlib.Algebra.Group.Commute.Defs

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

English

If a commutes with b, then a*(b*c) = b*(a*c).

Русский

Если a коммутирует с b, то a*(b*c) = b*(a*c).

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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