proposition: Lemma freeP n (X : n.-tuple vT) : reflect (forall k, \sum_(i < n) k i *: X`_i = 0 -> (forall i, k i = 0)) (free X).
proof: Proof. rewrite free_b2mx; apply: (iffP idP) => [t_free k kt0 i | t_free]. suffices /rowP/(_ i): \row_i k i = 0 by rewrite !mxE. by apply/(row_free_inj t_free)/r2v_inj; rewrite mul0mx -lin_b2mx kt0 linear0. rewrite -kermx_eq0; apply/rowV0P=> rk /sub_kermxP kt0. by apply/rowP=> i; rewrite mxE {}t_free // mul_b2mx kt0 linear0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)