instCommGroup — Mathlib

English

If G and H are CommGroup, then G × H is a CommGroup; the product group is commutative componentwise.

Русский

Если G и H — коммутативные группы, то G × H — коммутативная группа; произведение с координатной структурой является коммутативной группой.

LaTeX

$$$\mathrm{CommGroup}(G) \wedge \mathrm{CommGroup}(H) \implies \mathrm{CommGroup}(G \times H)$$$

Lean4

@[to_additive]
instance instCommGroup [CommGroup G] [CommGroup H] : CommGroup (G × H) :=
  { mul_comm := fun ⟨g₁, h₁⟩ ⟨_, _⟩ => by rw [mk_mul_mk, mk_mul_mk, mul_comm g₁, mul_comm h₁] }

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