fact: Definition determinant n (A : matrix R n n) := \big[radd/0]_(s : 'S_n) ((-(1:R)) ^+ s * \prod_(i < n) A i (s i)).
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms