no goals
m : Type ?u.1185437
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
σ : Perm n
⊢ det (PEquiv.toMatrix (toPEquiv σ)) = ↑↑(↑sign σ)
rw [← Matrix.mul_one (σ.toPEquiv.toMatrix : Matrix n n R), PEquiv.toPEquiv_mul_matrix,
  det_permute, det_one, mul_one]