Involutive and cardinality of fixed points mod 2

Stream: Is there code for X?

[Yongyi Chen]

Do we have these

import Mathlib

variable [Fintype α] [DecidableEq α] (f : α → α) (hf : f.Involutive)

example (h : f.fixedPoints = ∅) : Even (Fintype.card α) := by sorry
example: Fintype.card α ≡ Fintype.card (f.fixedPoints) [ZMOD 2] := by sorry

? I tried proving the first one myself using setoids but failed.

[Alex J. Best]

docs#Equiv.Perm.card_fixedPoints_modEq should be relevant I think

[Yongyi Chen]

That's great! After changing ZMOD to MOD I came up with

lemma lem (hf : f.Involutive) : Fintype.card α ≡ Fintype.card (f.fixedPoints) [MOD 2] := by
  apply Equiv.Perm.card_fixedPoints_modEq
  case n => exact 1
  case hf => simp [sq, Function.End.mul_def]; exact Function.Involutive.comp_self hf

example (hf : f.Involutive) (h : f.fixedPoints = ∅) : Even (Fintype.card α) := by
  have := lem f hf
  simp_all
  exact Nat.even_iff.mpr this