instCommSemigroup — Mathlib

English

If G and H are commutative semigroups, then G × H is a commutative semigroup; coordinates commute.

Русский

Если G и H коммутативны, то их произведение G × H также коммутативно; компоненты commute.

LaTeX

$$$(g_1,h_1) \cdot (g_2,h_2) = (g_2,h_2) \cdot (g_1,h_1)$$$

Lean4

@[to_additive]
instance instCommSemigroup [CommSemigroup G] [CommSemigroup H] : CommSemigroup (G × H) where
  mul_comm _ _ := by ext <;> exact mul_comm ..

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