proposition: Lemma hommx_linear : linear hommx.
proof: Proof. rewrite /hommx; move=> x A B; apply/lfunP=> u; do !rewrite lfunE/=. by rewrite /funmx mulmxDr -scalemxAr linearP. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_algebra all_solvable)