fact: Definition codiagonalizablePfull n (As : seq 'M[F]_n) : codiagonalizable As <-> exists m, exists2 P : 'M_(m, n), row_full P & all [pred A | diagonalizable_for P A] As.
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)