to_isCommutative

Mathlib.Algebra.Group.Basic

URI: https://scilib.ai/kg/mathlib#CommMagma.to_isCommutative

English

In a commutative magma, multiplication is commutative: ab = ba.

Русский

В коммутативном магме умножение коммутативно: ab = ba.

LaTeX

$$$a \cdot b = b \cdot a$$$

Lean4

@[to_additive]
instance to_isCommutative [CommMagma G] : Std.Commutative (α := G) (· * ·) :=
  ⟨mul_comm⟩

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

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

Разделы

Аффилиация

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