proposition: Lemma detDl (p1 p2 p3 q1 q2 q3 r1 r2 r3 : R) : det (p1+p2, p3) (q1+q2, q3) (r1+r2, r3) = det (p1, p3) (q1, q3) (r1, r3) + det (p2, p3) (q2, q3) (r2, r3).
proof: Proof. by rewrite !develop_det/=; ring. Qed.
imports: axiomsKnuth mathcomp(all_ssreflect ssralg matrix ssrnum vector reals) mathcomp(normedtype order) mathcomp.algebra_tactics(ring) mathcomp.zify(zify)