refl

Mathlib.Algebra.Group.Commute.Defs

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

← MathLib Explorer

English

Any element commutes with itself.

Русский

Любой элемент коммутирует с самим собой.

LaTeX

$$$\\forall a,\\ a a = a a$$$

Lean4

/-- Any element commutes with itself. -/
@[to_additive (attr := refl, simp) /-- Any element commutes with itself. -/
    ]
protected theorem refl (a : S) : Commute a a :=
  Eq.refl (a * a)

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

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

Разделы

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

Аффилиация

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