proposition: Lemma L1 m (a d: R) (l: 'rV[R]_m) (c: 'cV[R]_m) (M: 'M[R]_m): \det (block_mx d%:M l (a *: c) (a *: M)) = a ^+ m * \det (block_mx d%:M l c M).
proof: Proof. set X := block_mx d%:M l c M. have huniq : uniq (map (lift 0) (enum 'I_m)). - rewrite map_inj_in_uniq; first exact: enum_uniq. by move => i j hi hj /= /lift_inj. have htool : forall s, 0 \notin map (lift 0) s by move => n /=; elim. have -> : block_mx d%:M l (a *: c) (a *: M) = foldl (fun N i => line_scale i a N) X (map (lift 0) (enum 'I_m)). - apply/row_matrixP => i. case: (lines_scale_row a X huniq) => hl hr. move: (hl i) (hr i) => {hl hr}. case: (splitP i) => j. + rewrite [j]ord1 {j} => hi. have {i hi}-> : i = 0 by apply/ord_inj. move => _ /= ->; last exact: htool. apply/rowP => j; rewrite !mxE. by case: splitP. move => hi. have {i hi}-> : i = lift 0 j by apply/ord_inj. move => -> /=. + move => _. apply/rowP => k; rewrite !mxE. case: splitP => x; first by rewrite [x]ord1. rewrite !mxE => _. case: splitP => y; by rewrite !mxE. rewrite mem_map ?mem_enum //. by apply/lift_inj. by rewrite det_lines_scale size_map size_enum_ord /=. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice) mathcomp(matrix bigop zmodp mxalgebra poly polydiv mxpoly) ssrcomplements dvdring minor atomic_operations