mathlib

ce34ae6a - chore(linear_algebra/alternating): golf a proof (#5666)

chore(linear_algebra/alternating): golf a proof (#5666) `sign_mul` seems to have been marked `simp` recently, making it not necessary to include in `simp` calls.