Odd_Order_Group_Element_is_Square
Provedgroup-theoryorderproofwikisquare
In a group, if the order of x is odd, then x is a square (there exists y with y^2 = x).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Odd_Order_Group_Element_is_Square {G : Type _} [Group G] (x : G) (hodd : Odd (orderOf x)) : ∃ y : G, y * y = x := by sorrySource