ofIsMulCommutative

Mathlib.Algebra.Group.Defs

URI: https://scilib.ai/kg/mathlib#CommGroup.ofIsMulCommutative

English

If a group G satisfies IsMulCommutative, then G is a CommGroup.

Русский

Если группу G удовлетворяет IsMulCommutative, то она является CommGroup.

LaTeX

$$$\\\\forall G \\\\forall [Group G] [IsMulCommutative G], \\\\operatorname{CommGroup} G$$$

Lean4

@[to_additive]
instance (priority := 100) ofIsMulCommutative {G : Type*} [Group G] [IsMulCommutative G] : CommGroup G where

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

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

Разделы

Аффилиация

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