toCommGroup — Mathlib

English

The subgroup H has a natural inclusion into G given by the subtype map, i.e., the map H → G sends x ∈ H to x ∈ G.

Русский

У подгруппы H есть естественное включение в G через подтип: отображение H → G отправляет x ∈ H в x ∈ G.

LaTeX

$$$\text{the inclusion } H \to G \text{ is the map } x \mapsto x$$$

Lean4

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

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