`BookProof.ChapterA3r.trace_permMat` {N : ℕ} (σ : Equiv.Perm (Fin N)) : Matrix.trace (permMat σ) = ((Finset.univ.filter (fun a : Idx N => a ∘ σ = a)).card : ℂ)

Initializing...

`BookProof.ChapterA3r.trace_permMat` {N : ℕ} (σ : Equiv.Perm (Fin N)) : Matrix.trace (permMat σ) = ((Finset.univ.filter (fun a : Idx N => a ∘ σ = a)).card : ℂ) · Prove2Me