Identity_is_only_Idempotent_Element_in_Group
Provedgroup-theoryidempotenceidentity-elementsproofwiki
The identity is the only idempotent element in a group.
Preamble
import Mathlib.Algebra.Group.Defs
Formal statement
theorem Identity_is_only_Idempotent_Element_in_Group {G : Type _} [Group G] (x : G) (h : x * x = x) : x = 1 := by sorrySource