Even_Order_Group_has_Order_2_Element
Provedeven-ordergroup-theoryorderproofwiki
In a group of even order, there exists an element of order 2, i.e., an element x ≠ e with x^2 = e.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Even_Order_Group_has_Order_2_Element {G : Type _} [Group G] [Fintype G] (heven : Even (Fintype.card G)) : ∃ x : G, x ≠ 1 ∧ x * x = 1 := by sorrySource