proposition: Lemma minor_diag_mx_seq : let l := minn m n in forall (f g : 'I_k -> 'I_l), let f' i := widen_minl (f i) in let g' i := widen_minr (g i) in injective f -> injective g -> {subset codom f <= codom g} -> minor f' g' (diag_mx_seq m n s) %= \prod_i s`_(f i).
proof: Proof. rewrite /minor. elim: k=>[f g|j IHj f g Hf Hg Hfg]; first by rewrite det_mx00 big_ord0. have := perm_eq_image Hf Hg Hfg. have Ht : size (codom g) == j.+1 by rewrite size_codom card_ord. have -> : image g 'I_j.+1 = Tuple Ht by []. case/tuple_permP=> p Hp. have Hfg0 i : g (p i) = f i. have He: (i < #|'I_j.+1|)%N by rewrite card_ord. have {2}->: i = enum_val (Ordinal He) by rewrite enum_val_ord; apply: ord_inj. rewrite -(nth_image (f ord0)) Hp -tnth_nth tnth_mktuple (tnth_nth (f ord0)). by rewrite /= codomE (nth_map ord0) ?nth_ord_enum // size_enum_ord. rewrite (expand_det_row _ ((p^-1)%g ord0)) big_ord_recl big1=>[|i _]. rewrite /cofactor !mxE. set B := diag_mx_seq _ _ _. set M := row' _ _. pose f2 x := f (lift ((p^-1)%g ord0) x). pose g2 x := g (lift ord0 x). have Hf2: injective f2. by apply/(inj_comp Hf)/lift_inj. have Hg2: injective g2. by apply/(inj_comp Hg)/lift_inj. pose f' i := widen_ord (geq_minl m n) (f2 i). pose g' i := widen_ord (geq_minr m n) (g2 i). have ->: M = submatrix f' g' B. by apply/matrixP=> r t; rewrite !mxE. have Hfg2: {subset codom f2 <= codom g2}. move=> x /codomP [y ->]. rewrite codomE /f2 /g2 -Hfg0 map_comp (mem_map Hg). set i := p _. have:= mem_ord_enum i. rewrite -enum_ord_enum enum_ordSl in_cons -(permKV p ord0). by rewrite /i (inj_eq (@perm_inj _ _)) eq_sym (negbTE (neq_lift _ _)). rewrite addr0 (bigD1 ((p^-1)%g ord0)) //= -Hfg0 permKV eqxx eqd_mull //. rewrite -[X in _ %= X]mul1r eqd_mul ?eqd1 ?unitrX ?unitrN ?unitr1 //. rewrite (eq_bigl (fun i => (p^-1)%g ord0 != i)) ?big_lift_ord /=; last first. by move=> i /=; rewrite eq_sym. exact: (IHj _ _ Hf2 Hg2 Hfg2). rewrite !mxE /= (inj_eq (@ord_inj _)) -Hfg0 (inj_eq Hg) permKV. by rewrite (negbTE (neq_lift _ _)) mul0r. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra) mathcomp(all_fingroup) mathcomp(all_real_closed) CoqEAL(binetcauchy ssrcomplements mxstructure minor) CoqEAL(smith dvdring polydvd) CoqEAL(similar perm_eq_image)