Identity_is_Only_Group_Element_of_Order_1
Provedgroup-theoryorderproofwiki
In every group, the identity, and only the identity, has order 1.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Identity_is_Only_Group_Element_of_Order_1 {G : Type _} [Group G] (x : G) : orderOf x = 1 ↔ x = 1 := by sorrySource