English
For any x,y in a group, y ∈ closure({x}) iff ∃ n ∈ ℤ, x^n = y.
Русский
Для любых x,y в группе: y ∈ closure({x}) тогда и только тогда, когда ∃ n ∈ ℤ, x^n = y.
LaTeX
$$$ y \in \mathrm{closure}(\{x\}) \iff \exists n \in \mathbb{Z}, x^{n} = y $$$
Lean4
/-- The subgroup generated by an element of a group equals the set of integer number powers of
the element. -/
@[to_additive /-- The `AddSubgroup` generated by an element of an `AddGroup` equals the set of
natural number multiples of the element. -/
]
theorem mem_closure_singleton {x y : G} : y ∈ closure ({ x } : Set G) ↔ ∃ n : ℤ, x ^ n = y :=
by
refine
⟨fun hy => closure_induction ?_ ?_ ?_ ?_ hy, fun ⟨n, hn⟩ => hn ▸ zpow_mem (subset_closure <| mem_singleton x) n⟩
· intro y hy
rw [eq_of_mem_singleton hy]
exact ⟨1, zpow_one x⟩
· exact ⟨0, zpow_zero x⟩
· rintro _ _ _ _ ⟨n, rfl⟩ ⟨m, rfl⟩
exact ⟨n + m, zpow_add x n m⟩
rintro _ _ ⟨n, rfl⟩
exact ⟨-n, zpow_neg x n⟩
