toGroup — Mathlib

English

A subgroup H of a group G is itself a group under the same operation.

Русский

Подгруппа H группы G сама образует группу под тем же бинарным умножением (операцией).

LaTeX

$$$$ \\text{If } H \\le G, \\text{ then } H \\text{ is a group with the inherited operation from } G. $$$$

Lean4

/-- A subgroup of a group inherits a group structure. -/
@[to_additive /-- An additive subgroup of an `AddGroup` inherits an `AddGroup` structure. -/
    ]
instance (priority := 75) toGroup : Group H :=
  fast_instance%Subtype.coe_injective.group _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl)
      fun _ _ => rfl

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