instMulOpposite

Mathlib.Algebra.Group.UniqueProds.Basic

URI: https://scilib.ai/kg/mathlib#UniqueProds.instMulOpposite

English

If G has UniqueProds, then its opposite Gᵐᵒᵖ has UniqueProds.

Русский

Если у G есть UniqueProds, то у Gᵐᵒᵖ тоже есть UniqueProds.

LaTeX

$$$ [\\mathrm{UniqueProds }G] \\Rightarrow \\mathrm{UniqueProds}(G^{\\mathrm{op}}). $$$

Lean4

@[to_additive]
instance [h : UniqueProds G] : UniqueProds Gᵐᵒᵖ :=
  of_mulOpposite <| (MulEquiv.opOp G).uniqueProds_iff.mp h

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

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

Разделы

Аффилиация

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