Identity_of_Subgroup
Provedidentity-elementsproofwikisubgroups
Let G be a group whose identity is e. Let H be a subgroup of G. Then the identity of H is also e.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Identity_of_Subgroup {G : Type _} [Group G] (H : Subgroup G) : (1 : G) ∈ H := by sorrySource