instGroup — Mathlib

English

If G and H are groups, then G × H is a group with inverse (g,h)^{-1} = (g^{-1}, h^{-1}).

Русский

Если G и H — группы, то G × H — группа, а обратное элемента пары задается по координатам: (g,h)^{-1}=(g^{-1},h^{-1}).

LaTeX

$$[Group G] [Group H] ⇒ (g,h)^{-1} = (g^{-1}, h^{-1})$$

Lean4

@[to_additive]
instance instGroup [Group G] [Group H] : Group (G × H) where inv_mul_cancel _ := by ext <;> exact inv_mul_cancel _

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