proposition: Lemma size_Frobenius_seq n (A : 'M[F]_n) : size (Frobenius_seq A) = n.
proof: Proof. by rewrite size_map size_Smith_seq // -size_poly_eq0 size_char_poly. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra) mathcomp(all_fingroup) mathcomp(all_real_closed) CoqEAL(binetcauchy ssrcomplements mxstructure minor) CoqEAL(smith dvdring polydvd) CoqEAL(similar perm_eq_image companion closed_poly smith_complements)