Subgroup_of_Cyclic_Group_is_Cyclic

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

cyclic-groupsproofwikisubgroup-of-cyclic-group-is-cyclicsubgroups

Let $G$ be a cyclic group. Let $H$ be a subgroup of $G$ . Then $H$ is cyclic.

Preamble

import Mathlib.GroupTheory.SpecificGroups.Cyclic

Formal statement

theorem Subgroup_of_Cyclic_Group_is_Cyclic {G : Type*} [Group G] [IsCyclic G] (H : Subgroup G) : IsCyclic H := by sorry

Source