mul_rotate'

Mathlib.Algebra.Group.Basic

URI: https://scilib.ai/kg/mathlib#mul_rotate'

English

In a commutative semigroup, a (b c) = b (c a).

Русский

В коммутативной полугруппе выполняется a (b c) = b (c a).

LaTeX

$$$a (b c) = b (c a)$$$

Lean4

@[to_additive]
theorem mul_rotate' (a b c : G) : a * (b * c) = b * (c * a) := by simp only [mul_left_comm, mul_comm]

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

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

Разделы

Аффилиация

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