Matrix determinant

The determinant $d e t 𝐴 \in 𝕂$ of a matrix $𝐴 \in M 𝑛, 𝑛 𝕂$ is a scalar quantity uniquely defined by its properties, namely: #m/def/linalg

$d e t 𝟙 = 1$ , where $𝟙$ is the identity matrix;
The exchange of two rows of $𝐴$ multiplies the determinant by $- 1$ ;
Multiplying a row by a scalar multiplies the determinant by that scalar;
Adding any multiple of a different row to a given row does not affect the determinant.

Leibniz formula

The determinant of a matrix $𝐴 = (𝑎 𝑖 𝑗) \in M 𝑛, 𝑛 𝕂$ is given by #m/thm/linalg

d e t (𝑎 𝑖 𝑗) = \sum 𝜏 \in S 𝑛 (s g n 𝜏) 𝑛 \prod 𝑖 = 1 𝑎 𝑖 𝜏 (𝑖) = \sum 𝜏 \in S 𝑛 (s g n 𝜏) 𝑛 \prod 𝑖 = 1 𝑎 𝜏 (𝑖) 𝑖

which is known as the Leibniz formula for the determinant.

Proof

#missing/proof