theorem Equiv.Perm.ToPequiv.toMatrix_mem_unitaryGroup {n : Type u_1} [DecidableEq n] [Fintype n] {𝕜 : Type u_2} [CommRing 𝕜] [StarRing 𝕜] (σ : Perm n) : (toPEquiv σ).toMatrix ∈ Matrix.unitaryGroup n 𝕜