symm

Mathlib.Algebra.Group.Commute.Defs

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

← MathLib Explorer

English

If a commutes with b, then b commutes with a.

Русский

Если a коммутирует с b, то b коммутирует с a.

LaTeX

$$$\\forall a,b \\in S,\\ Commute a b \\rightarrow Commute b a$$$

Lean4

/-- If `a` commutes with `b`, then `b` commutes with `a`. -/
@[to_additive (attr := symm) /-- If `a` commutes with `b`, then `b` commutes with `a`. -/
    ]
protected theorem symm {a b : S} (h : Commute a b) : Commute b a :=
  Eq.symm h

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

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

Разделы

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

Аффилиация

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