proposition: Lemma detZl (p1 p2 q1 q2 r1 r2 t : R) : det (t * p1, p2) (t * q1, q2) (t * r1, r2) = t * det (p1, p2) (q1, q2) (r1, r2).
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)