Fixed points of involutions on sets of odd order

Stream: Is there code for X?

[Stepan Nesterov]

I am trying to formalize the intended solution to the following exercise in Dummit-Foote:

theorem exercise1_1_31 [Fintype G] (h : Even (Fintype.card G)) : ∃ x : G, orderOf x = 2 := by
  sorry

Which is to say, to consider an involution g => g^-1 on the set G\{1}, and conclude that it has a fixed point because the set is of odd order. Is this a theorem in mathlib?

[Kenny Lau]

@Stepan Nesterov you can't find it because it's true in a higher generality :slight_smile:
exists_prime_orderOf_dvd_card:

theorem exists_prime_orderOf_dvd_card {G : Type u_3} [Group G] [Fintype G]
    (p : ℕ) [hp : Fact (Nat.Prime p)] (hdvd : p ∣ Fintype.card G) :
  ∃ (x : G), orderOf x = p

[Kenny Lau]

this is in fact the building block of Sylow theory

[Stepan Nesterov]

Ah, so the result I’m looking for is exists_fixed_point_of_prime is the same file
Thx!