proposition: Lemma key_lemma m d (l: 'rV[R]_m) (c: 'cV[R]_m) M: d ^+ m * \det (block_mx d%:M l c M) = d * \det (d *: M - c *m l).
proof: Proof. by rewrite -L1 (L3 d l (d *: c) c (d *: M)) subrr det_ublock det_scalar1. 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