centerToMulOpposite

Mathlib.GroupTheory.Submonoid.Center

URI: https://scilib.ai/kg/mathlib#Submonoid.centerToMulOpposite

Lean4

/-- The center of a monoid is isomorphic to the center of its opposite. -/
@[to_additive (attr := simps!) /-- The center of an additive monoid is isomorphic to the center of its opposite. -/
    ]
def centerToMulOpposite [MulOneClass M] : center M ≃* center Mᵐᵒᵖ :=
  Subsemigroup.centerToMulOpposite

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

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

Разделы

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

Аффилиация

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