proposition: Lemma minor1 m n (A : 'M[R]_(m,n)) i j : minor (fun (_ : 'I_1) => i) (fun _ => j) A = A i j.
proof: Proof. by rewrite /minor [submatrix _ _ _]mx11_scalar det_scalar1 !mxE. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path ssralg) mathcomp(fintype perm choice finfun matrix bigop zmodp poly mxpoly)