Group_is_Subgroup_of_Itself
Provedproofwikisubgroups
Let G be a group. Then G is a subgroup of itself.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Group_is_Subgroup_of_Itself {G : Type _} [Group G] (g : G) : g ∈ (⊤ : Subgroup G) := by sorrySource