proposition: Lemma vecof_delta i : vecof (delta_mx 0 i) = e`_i.
proof: Proof. rewrite /vecof (bigD1 i)//= mxE !eqxx scale1r big1 ?addr0// => j neq_ji. by rewrite mxE (negPf neq_ji) andbF scale0r. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_algebra all_solvable)