LeanPool.Monlib4.Preq.Equiv #
Imported Lean Pool material for LeanPool.Monlib4.Preq.Equiv.
theorem
Equiv.Perm.ToPequiv.toMatrix_mem_unitaryGroup
{n : Type u_1}
[DecidableEq n]
[Fintype n]
{𝕜 : Type u_2}
[CommRing 𝕜]
[StarRing 𝕜]
(σ : Perm n)
: