Existence_of_Unique_Subgroup_Generated_by_Subset
Provedgenerated-substructuregroup-theoryproofwikisubgroup
Let G be a group and S a nonempty subset of G. Then the subgroup generated by S exists and is unique, and it is the smallest subgroup containing S.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Existence_of_Unique_Subgroup_Generated_by_Subset {G : Type _} [Group G] (S : Set G) : ∃ H : Subgroup G, (∀ s ∈ S, s ∈ H) ∧ ∀ K : Subgroup G, (∀ s ∈ S, s ∈ K) → H ≤ K := by sorrySource