eq

Mathlib.Algebra.Group.Commute.Defs

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

← MathLib Explorer

English

If a and b commute, then ab = ba.

Русский

Если элементы a и b коммутируют, то ab = ba.

LaTeX

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

Lean4

/-- Equality behind `Commute a b`; useful for rewriting. -/
@[to_additive /-- Equality behind `AddCommute a b`; useful for rewriting. -/
    ]
protected theorem eq {a b : S} (h : Commute a b) : a * b = b * a :=
  h

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

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

Разделы

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

Аффилиация

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