theorem Determinant.det_leibniz_column {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} [CommRing R] (M : Matrix n n R) : M.det = ∑ σ : Equiv.Perm n, ↑(Equiv.Perm.sign σ) • ∏ i : n, M i (σ i)