instGroup

Mathlib.Algebra.Group.Opposite

URI: https://scilib.ai/kg/mathlib#MulOpposite.instGroup

← MathLib Explorer

English

If α is a group, then the opposite αᵐᵒᵖ is a group.

Русский

Если α является группой, то αᵐᵒᵖ является группой.

LaTeX

$$$\text{Group}(\alpha) \Rightarrow \text{Group}(\alpha^{op})$$$

Lean4

@[to_additive]
instance instGroup [Group α] : Group αᵐᵒᵖ
    where
  toDivInvMonoid := instDivInvMonoid
  inv_mul_cancel _ := unop_injective <| mul_inv_cancel _

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

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

Разделы

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

Аффилиация

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