proposition: Lemma codiagonalizable1 n (A : 'M[F]_n) : codiagonalizable [:: A] <-> diagonalizable A.
proof: Proof. by split=> -[P Punit PA]; exists P; move: PA; rewrite //= andbT. 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)