Inverse_Element_is_Power_of_Order_Less_1
Provedgroup-theoryinverseorderproofwiki
Let G be a group and g an element of finite order n. Then g^(n-1) = g⁻¹.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Inverse_Element_is_Power_of_Order_Less_1 {G : Type _} [Group G] (g : G) (n : ℕ) (hn : orderOf g = n) (hn0 : 0 < n) : g ^ (n - 1) = g⁻¹ := by sorrySource