all

Mathlib.Algebra.Group.Commute.Defs

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

English

In a commutative magma, any two elements commute.

Русский

В комммагме с коммутативной операцией любые два элемента коммутируют.

LaTeX

$$$\\forall S [CommMagma S],\\ \forall a,b \\in S,\\ Commute a b$$$

Lean4

@[to_additive]
protected theorem all [CommMagma S] (a b : S) : Commute a b :=
  mul_comm a b

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

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

Разделы

Аффилиация

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