proposition: Lemma rowmxof_sub u M : (rowmxof e u <= M)%MS = (u \in vsof M).
proof: Proof. apply/submxP/memv_imgP => [[v /(canRL (rowmxofK _)) ->//]|[v _ ->]]{u}. by exists (vecof e v); rewrite ?memvf// -vecof_mul. by exists (rowmxof e v); rewrite -rowmxof_mul. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_algebra all_solvable)