proposition: Theorem fin_Csubring_Aint S n (Y : n.-tuple algC) : mulr_closed S -> (forall x, reflect (inIntSpan Y x) (x \in S)) -> {subset S <= Aint}.
proof: Proof. move=> mulS. pose Sm := GRing.isMulClosed.Build _ _ mulS. pose SC : mulrClosed _ := HB.pack S Sm. have ZP_C c: (ZtoC c)%:P \is a polyOver Num.int_num_subdef. by rewrite raddfMz rpred_int. move=> S_P x Sx; pose v := \row_(i < n) Y`_i. have [v0 | nz_v] := eqVneq v 0. case/S_P: Sx => {}x ->; rewrite big1 ?isAlgInt0 // => i _. by have /rowP/(_ i)/[!mxE] -> := v0; rewrite mul0rz. have sYS (i : 'I_n): x * Y`_i \in SC. by rewrite rpredM //; apply/S_P/Cint_spanP/mem_Cint_span/memt_nth. pose A := \matrix_(i, j < n) sval (sig_eqW (S_P _ (sYS j))) i. pose p := char_poly (map_mx ZtoC A). have: p \is a polyOver Num.int_num_subdef. rewrite rpred_sum // => s _; rewrite rpredMsign rpred_prod // => j _. by rewrite !mxE /= rpredB ?rpredMn ?polyOverX. apply: root_monic_Aint (char_poly_monic _). rewrite -eigenvalue_root_char; apply/eigenvalueP; exists v => //. apply/rowP=> j; case dAj: (sig_eqW (S_P _ (sYS j))) => [a DxY]. by rewrite !mxE DxY; apply: eq_bigr => i _; rewrite !mxE dAj /= mulrzr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly polydiv ssrnum ssrint archimedean rat) mathcomp(finalg zmodp matrix mxalgebra mxpoly vector intdiv) mathcomp(falgebra fieldext separable galois algC cyclotomic)