commGroup_isMulCommutative — Mathlib

English

A subgroup of a commutative group is itself commutative.

Русский

Подгруппа коммутативной группы сама по себе коммутативна.

LaTeX

$$$G \\text{ abelian} \\Rightarrow \\forall x,y \\in H, x y = y x$$$

Lean4

/-- A subgroup of a commutative group is commutative. -/
@[to_additive /-- A subgroup of a commutative group is commutative. -/
    ]
instance commGroup_isMulCommutative {G : Type*} [CommGroup G] (H : Subgroup G) : IsMulCommutative H :=
  ⟨CommMagma.to_isCommutative⟩

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