Order_of_Element_Divides_Order_of_Finite_Group
Provedgroup-theorylagrangeorderproofwiki
In a finite group, the order of every element divides the order of the group.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Order_of_Element_Divides_Order_of_Finite_Group {G : Type _} [Group G] [Fintype G] (x : G) : orderOf x ∣ Fintype.card G := by sorrySource