Element_of_Finite_Group_is_of_Finite_Order
Provedfinite-groupgroup-theoryorderproofwiki
In any finite group, each element has finite order (i.e., orderOf x > 0).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Element_of_Finite_Group_is_of_Finite_Order {G : Type _} [Group G] [Fintype G] (x : G) : 0 < orderOf x := by sorrySource