zpowers — Mathlib

English

The subgroup generated by g consists exactly of integer powers of g: ⟨g⟩ = { g^n : n ∈ ℤ }.

Русский

Подгруппа, порождаемая g, состоит ровно из целочисленных степеней g: ⟨g⟩ = { g^n : n ∈ ℤ }.

LaTeX

$$$ \langle g \rangle = \{ g^{n} : n \in \mathbb{Z} \}$$$

Lean4

/-- The subgroup generated by an element. -/
@[to_additive /-- The additive subgroup generated by an element. -/
    ]
def zpowers (g : G) : Subgroup G where
  carrier := Set.range (g ^ · : ℤ → G)
  one_mem' := ⟨0, zpow_zero g⟩
  mul_mem' := by rintro _ _ ⟨a, rfl⟩ ⟨b, rfl⟩; exact ⟨a + b, zpow_add ..⟩
  inv_mem' := by rintro _ ⟨a, rfl⟩; exact ⟨-a, zpow_neg ..⟩

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