opposite_smulCommClass'

Mathlib.Algebra.Group.Action.Opposite

URI: https://scilib.ai/kg/mathlib#Semigroup.opposite_smulCommClass'

English

There is a symmetry SMulCommClass α αᵐᵒᵖ α: the actions of α and αᵐᵒᵖ commute on α.

Русский

Существуют гомоморфизмы SMulCommClass α αᵐᵒᵖ α, т.е. действия α и αᵐᵒᵖ коммутируют на α.

LaTeX

$$$\text{SMulCommClass } α \ α^{\mathrm{op}} α$$$

Lean4

@[to_additive]
instance opposite_smulCommClass' [Semigroup α] : SMulCommClass α αᵐᵒᵖ α :=
  SMulCommClass.symm _ _ _

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

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

Разделы

Аффилиация

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