Element_to_Power_of_Group_Order_is_Identity
Provedgroup-theorylagrangeorderproofwiki
Let G be a finite group of order n. Then for all g in G, g^n = e.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Element_to_Power_of_Group_Order_is_Identity {G : Type _} [Group G] [Fintype G] (g : G) : g ^ Fintype.card G = 1 := by sorrySource