no goals
m : Type ?u.1058568
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
σ : Perm n
M : Matrix n n R
⊢ ↑sign σ • ↑detRowAlternating M = ↑↑(↑sign σ) * det M
simp [Units.smul_def]