proposition: Lemma coord_free n (X : n.-tuple vT) (i j : 'I_n) : free X -> coord X j (X`_i) = (i == j)%:R.
proof: Proof. rewrite unlock free_b2mx => /row_freeP[Ct CtK]; rewrite -row_b2mx. by rewrite -row_mul -[pinvmx _]mulmx1 -CtK 3!mulmxA mulmxKpV // CtK !mxE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)