instMulOpposite

Mathlib.Algebra.Group.UniqueProds.Basic

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

English

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

Русский

Если G имеет TwoUniqueProds, то у Gᵐᵒᵖ то же свойство.

LaTeX

$$$ \\forall G\\,[\\mathrm{Mul }G][\\mathrm{TwoUniqueProds }G] \\Rightarrow \\mathrm{TwoUniqueProds}(G^{\\mathrm{op}}). $$$

Lean4

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

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

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

Разделы

Аффилиация

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