`BookProof.ChapterA3u.card_fixedTuples` {N : ℕ} (σ : Equiv.Perm (Fin N)) : (Finset.univ.filter (fun a : Idx N => a ∘ σ = a)).card = 4 ^ ((N - σ.cycleType.sum) + σ.cycleType.card)

Initializing...

`BookProof.ChapterA3u.card_fixedTuples` {N : ℕ} (σ : Equiv.Perm (Fin N)) : (Finset.univ.filter (fun a : Idx N => a ∘ σ = a)).card = 4 ^ ((N - σ.cycleType.sum) + σ.cycleType.card) · Prove2Me