right_comm

Mathlib.Algebra.Group.Center

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

← MathLib Explorer

English

If c is central, then a · b · c = a · c · b for all a, b.

Русский

Если c центральен, то для всех a, b верно a · b · c = a · c · b.

LaTeX

$$$a * b * c = a * c * b$$$

Lean4

@[to_additive]
protected theorem right_comm (h : IsMulCentral c) (a b) : a * b * c = a * c * b := by
  simp only [h.right_assoc, h.mid_assoc, (h.comm _).eq]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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