proposition: Lemma sum_size_inv_factors n (A : 'M[F]_n) : (\sum_(p <- invariant_factors A) (size p).-1 = n)%N.
proof: Proof. have {2}->: n = n.+1.-1 by []. rewrite -(size_char_poly A) -invf_char_poly (big_nth 0) [in RHS](big_nth 0). rewrite !big_mkord size_prod=> [|i _]; last first. by apply: (@invariant_factor_neq0 _ A); rewrite mem_nth. rewrite subSKn -sum1_card; apply/eqP. set s := (\sum_(i in _) 1)%N. rewrite -(eqn_add2r s) subnK. apply/eqP; rewrite -big_split /=; apply: eq_bigr=> i _. rewrite addn1 prednK // size_poly_gt0. by apply: (@invariant_factor_neq0 _ A); rewrite mem_nth. apply: leq_sum=> i _; rewrite size_poly_gt0. by apply: (@invariant_factor_neq0 _ A); rewrite mem_nth. 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)