proposition: Lemma determinant_multilinear : forall n (A B C : 'M_n) i0 b c, mx_row i0 A === b *m: mx_row i0 B +m c *m: mx_row i0 C -> mx_row' i0 B === mx_row' i0 A -> mx_row' i0 C === mx_row' i0 A -> \det A === b * \det B + c * \det C.
proof: Proof. move=> n A B C i0 b c; rewrite <- (mx_row_id (_ +m _)); move/mx_row_eq=> ABC. move/mx_row'_eq=> BA; move/mx_row'_eq=> CA; rewrite/determinant. setoid_rewrite (big_distrr _ b); setoid_rewrite (big_distrr _ c). rewrite <- big_split; apply eq_bigr => s _ /=. have Heq : forall x y z, req (b * (z * x) + c * (z * y)) (z * (b * x + c * y)) by move=> x y z; ring. rewrite -> Heq. apply rmul_morph; first by reflexivity. setoid_rewrite (bigD1 (j:=i0))=>//=. rewrite -> (ABC _). rewrite/mx_row/addmx/scalemx. transitivity ((b * B i0 (s i0)) * \prod_(i < n | i != i0) A i (s i) + c * (C i0 (s i0) * \prod_(i < n | i != i0) A i (s i))). set tmp := reducebig _ _ _ _ _; ring. apply radd_morph. ring_simplify; apply rmul_morph; first by reflexivity. by apply eq_bigr => i neq; symmetry; apply BA. ring_simplify; apply rmul_morph; first by reflexivity. by apply eq_bigr => i neq; symmetry; apply CA. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms