proposition: Lemma diagonalizable_for_row_base m n (P : 'M[F]_(m, n)) (A : 'M_n) : diagonalizable_for (row_base P) A = is_diag_mx (restrictmx P A).
proof: Proof. by []. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(div fintype tuple finfun bigop fingroup perm) mathcomp(ssralg zmodp matrix mxalgebra poly polydiv)