proposition: Lemma line_scale_eq : forall n m k a (M: 'M[R]_(n,m)), line_scale k a M = line_scale_mx k a M.
proof: Proof. move => n m k a M; apply/matrixP => i j; rewrite !mxE. rewrite (bigD1 i) //= big1 /=; first by rewrite !mxE addr0 eqxx. by move => x /negbTE hx; rewrite !mxE [i == x]eq_sym hx mulr0n mul0r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(ssralg fintype perm choice) mathcomp(matrix bigop zmodp mxalgebra poly mxpoly)