proposition: Lemma complex_acf_axiom : GRing.closed_field_axiom [ringType of R[i]].
proof: Proof. move=> n c n_gt0; pose p := 'X^n - \poly_(i < n) c i. suff [x rpx] : exists x, root p x. exists x; move: rpx; rewrite /root /p hornerD hornerN hornerXn subr_eq0. by move=> /eqP ->; rewrite horner_poly. have p_monic : p \is monic. rewrite qualifE/= lead_coefDl ?lead_coefXn //. by rewrite size_opp size_polyXn ltnS size_poly. have sp_gt1 : (size p > 1)%N. by rewrite size_addl size_polyXn // size_opp ltnS size_poly. case: n n_gt0 p => //= n _ p in p_monic sp_gt1 *. have [] := Theorem7' (companionmx p); first by rewrite -(subnK sp_gt1) addn2. by move=> x; rewrite eigenvalue_root_char companionmxK //; exists x. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrint div ssrnum rat poly closed_field) mathcomp(polyrcf matrix mxalgebra tuple mxpoly zmodp binomial realalg) mathcomp(mxpoly)