proposition: Lemma line_scale_row_eq n m k a (M: 'M[R]_(n,m)): row k (line_scale k a M) = a *: row k M.
proof: Proof. by apply/rowP => i; rewrite !mxE eqxx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(ssralg fintype perm choice) mathcomp(matrix bigop zmodp mxalgebra poly mxpoly)