proposition: Lemma minor_eq0r (R' : comRingType) k1 m1 n1 (s1 : seq R') x : forall f (g : 'I_k1 -> 'I_n1) , m1 <= g x -> minor f g (diag_mx_seq m1 n1 s1) = 0.
proof: Proof. move=> f g H; rewrite /minor (expand_det_col _ x) big1 // => i _. by rewrite !mxE ltn_eqF ?mul0r // (leq_trans _ H). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path tuple) mathcomp(perm fingroup choice ssralg fintype finfun poly polydiv) mathcomp(bigop matrix zmodp mxalgebra) ssrcomplements dvdring mxstructure similar minor binetcauchy stronglydiscrete coherent