proposition: Lemma det_ublock : forall n1 n2 (Aul : 'M_(n1, n1)) (Aur : 'M_(n1, n2)) (Alr : 'M_(n2, n2)), \det (block_mx Aul Aur (@null_mx _ _ _ _ _ _ _ _ _ _ _ _) Alr : 'M_(n1 + n2)) === \det Aul * \det Alr.
proof: Proof. move=> n1 n2 Aul Aur Alr; elim: n1 => [|n1 IHn1] in Aul Aur *. have Heq : req (\det Aul) 1. by rewrite <- det1; apply determinant_morph; case. rewrite -> Heq; ring_simplify; apply determinant_morph=> i j; rewrite/block_mx/pastemx/trmx. case:splitP; [ by case | move=>i'; move/val_inj ->]. by case:splitP; [ case | move=> j'; move/val_inj ->; reflexivity]. rewrite -> (expand_det_col (block_mx Aul _ _ _) (lshift n2 ord0)). setoid_rewrite big_split_ord=>/=. setoid_rewrite (Radd_comm (r_rt (Ring:=r_ring))). setoid_rewrite (big1 (I:= ordinal_finType n2))=>[|i _]; last first. by rewrite -> block_mxEll; rewrite /null_mx; ring. setoid_rewrite (Radd_0_l (r_rt (Ring:=r_ring))). setoid_rewrite (expand_det_col Aul ord0). setoid_rewrite big_distrl. apply eq_bigr=>i _; rewrite -> block_mxEul. setoid_rewrite <- Rmul_assoc; last by apply r_ring. apply rmul_morph; first by reflexivity. rewrite/cofactor; rewrite <- (Rmul_assoc r_rt). rewrite <- (IHn1 (mx_row' i (mx_col' ord0 Aul)) (mx_row' i Aur)). have -> : (addn (nat_of_ord i) (@nat_of_ord (S n1) ord0) = nat_of_ord i) by done. apply rmul_morph; first by reflexivity. apply determinant_morph; rewrite {2}/block_mx; rewrite <- (mx_row'_paste i), (trmx_row' i). rewrite <- (mx_col'_lshift i), (trmx_col' (lshift n2 i)); apply (mx_row'_morph (lshift n2 i)). rewrite <- (mx_col'_lshift ord0 Aul), (trmx_col' (lshift n2 ord0) (pastemx Aul Aur)). rewrite /block_mx; rewrite <- trmx_row', mx_row'_paste; apply trmx_morph. apply pastemx_morph; first by reflexivity. rewrite <- trmx_col'; apply trmx_morph; rewrite -> mx_col'_lshift. apply pastemx_morph; last by reflexivity. by move=> i' j'; rewrite/mx_col'/lift/null_mx; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms