`BookProof.ChapterA3u.trace_permMat_pow` {N : ℕ} (σ : Equiv.Perm (Fin N)) : Matrix.trace (permMat σ) = ((4 ^ ((N - σ.cycleType.sum) + σ.cycleType.card) : ℕ) : ℂ)

Initializing...

`BookProof.ChapterA3u.trace_permMat_pow` {N : ℕ} (σ : Equiv.Perm (Fin N)) : Matrix.trace (permMat σ) = ((4 ^ ((N - σ.cycleType.sum) + σ.cycleType.card) : ℕ) : ℂ) · Prove2Me