mathlib3 documentation

monlib / preq.equiv

source
theorem equiv.perm.to_pequiv.to_matrix_mem_unitary_group {n : Type u_1} [decidable_eq n] [fintype n] {𝕜 : Type u_2} [comm_ring 𝕜] [star_ring 𝕜] (σ : equiv.perm n) :
(equiv.to_pequiv σ).to_matrix ∈ matrix.unitary_group n 𝕜