toCommGroup — Mathlib

English

A subgroup of a commutative group is a commutative group.

Русский

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

LaTeX

$$$$ H \\le G \\land G \\text{ is commutative } \\Rightarrow H \\text{ is commutative under the induced operation}. $$$$

Lean4

/-- A subgroup of a `CommGroup` is a `CommGroup`. -/
@[to_additive /-- An additive subgroup of an `AddCommGroup` is an `AddCommGroup`. -/
    ]
instance (priority := 75) toCommGroup {G : Type*} [CommGroup G] [SetLike S G] [SubgroupClass S G] : CommGroup H :=
  fast_instance%Subtype.coe_injective.commGroup _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl)
      fun _ _ => rfl

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