proposition: Lemma determinant_multilinear n (A B C : 'M[R]_n) i0 b c : row i0 A = b *: row i0 B + c *: row i0 C -> row' i0 B = row' i0 A -> row' i0 C = row' i0 A -> \det A = b * \det B + c * \det C.
proof: Proof. rewrite -[_ + _](row_id 0); move/row_eq=> ABC. move/row'_eq=> BA; move/row'_eq=> CA. rewrite !big_distrr -big_split; apply: eq_bigr => s _ /=. rewrite -!(mulrCA (_ ^+s)) -mulrDr; congr (_ * _). rewrite !(bigD1 i0 (_ : predT i0)) //= {}ABC !mxE mulrDl !mulrA. by congr (_ * _ + _ * _); apply: eq_bigr => i i0i; rewrite ?BA ?CA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg countalg finalg zmodp)