isCyclic_iff_exists_zpowers_eq_top

English

A subgroup H of a group G is cyclic iff there exists g with H = zpowers g.

Русский

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

LaTeX

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

Lean4

@[to_additive]
protected theorem isCyclic_iff_exists_zpowers_eq_top [Group α] (H : Subgroup α) :
    IsCyclic H ↔ ∃ g : α, Subgroup.zpowers g = H :=
  by
  rw [isCyclic_iff_exists_zpowers_eq_top]
  simp_rw [← (map_injective H.subtype_injective).eq_iff, ← MonoidHom.range_eq_map, H.range_subtype,
    MonoidHom.map_zpowers, Subtype.exists, coe_subtype, exists_prop]
  exact exists_congr fun g ↦ and_iff_right_of_imp fun h ↦ h ▸ mem_zpowers g

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