proposition: Lemma rowmxofE (i : 'I_n) : rowmxof e`_i = delta_mx 0 i.
proof: Proof. apply/rowP=> k; rewrite !mxE. by rewrite eqxx coord_free ?(basis_free e_basis)// eq_sym. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_algebra all_solvable)