isCyclic_iff_exists_zpowers_eq_top

English

A subgroup H is cyclic iff there exists g with H = zpowers g.

Русский

Подгруппа H циклична тогда и только тогда, когда существует g, для которого H = zpowers g.

LaTeX

$$$$\\operatorname{IsCyclic}(H) \\iff \\exists g, \\operatorname{Subgroup.zpowers}(g) = H.$$$$

Lean4

@[to_additive]
theorem isCyclic_iff_exists_zpowers_eq_top [Group α] : IsCyclic α ↔ ∃ g : α, zpowers g = ⊤ :=
  by
  simp only [eq_top_iff', mem_zpowers_iff]
  exact ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩

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