toGroup — Mathlib

English

The membership closure for zsmul: for all n ∈ ℤ and a ∈ H, n•a ∈ H.

Русский

Замкнутость по целочисленному масштабированию: для всех n ∈ ℤ и a ∈ H выполняется n•a ∈ H.

LaTeX

$$$\forall a \in H,\\forall n \in \mathbb{Z},\\ n \cdot a \in H$$$

Lean4

/-- A subgroup of a group inherits a group structure. -/
@[to_additive /-- An `AddSubgroup` of an `AddGroup` inherits an `AddGroup` structure. -/
    ]
instance toGroup {G : Type*} [Group G] (H : Subgroup G) : Group H :=
  fast_instance%Subtype.coe_injective.group _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl)
      fun _ _ => rfl

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