subgroup_cyclic — Mathlib

English

Every subgroup of the additive group of integers is cyclic; i.e., for any subgroup H ≤ ℤ there exists a ∈ ℤ with H = ⟨a⟩.

Русский

Любая подгруппа от (ℤ, +) циклична; то есть для любой H ≤ ℤ существует a ∈ ℤ такой, что H = ⟨a⟩.

LaTeX

$$$ \forall H \le \mathbb{Z}, \exists a \in \mathbb{Z}, H = \langle a \rangle. $$$

Lean4

/-- Every subgroup of `ℤ` is cyclic. -/
theorem subgroup_cyclic (H : AddSubgroup ℤ) : ∃ a, H = AddSubgroup.closure { a } :=
  have : Ioo (0 : ℤ) 1 = ∅ := eq_empty_of_forall_notMem fun _ hm => hm.1.not_ge (lt_add_one_iff.1 hm.2)
  AddSubgroup.cyclic_of_isolated_zero one_pos <| by simp [this]

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