fact: Definition cofactor n A (i j : 'I_n) : R := (-(1:R)) ^+ (i + j) * \det (mx_row' i (mx_col' j A)).
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms