zpowers_eq_closure — Mathlib

English

Let G be a group and g ∈ G. The cyclic subgroup generated by g, consisting of all integer powers g^n (n ∈ ℤ), is equal to the closure of the singleton {g}.

Русский

Пусть G — группа и g ∈ G. Циклическая подпгруппа, порождаемая элементом g, состоит из всех степеней g: g^n (n ∈ ℤ); она равна замыканию множества {g}.

LaTeX

$$$\langle g \rangle = \operatorname{closure}(\{g\})$$$

Lean4

@[to_additive]
theorem zpowers_eq_closure (g : G) : zpowers g = closure { g } :=
  by
  ext
  exact mem_closure_singleton.symm

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