proposition: Lemma memmx1 n (A : 'M_n) : (A \in mxvec 1%:M) = is_scalar_mx A.
proof: Proof. apply/sub_rVP/is_scalar_mxP=> [[a] | [a ->]]. by rewrite -linearZ scale_scalar_mx mulr1 => /(can_inj mxvecK); exists a. by exists a; rewrite -linearZ scale_scalar_mx mulr1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg finalg zmodp matrix)