proposition: Lemma dec_Cint_span (V : vectType algC) m (s : m.-tuple V) v : decidable (inIntSpan s v).
proof: Proof. have s_s (i : 'I_m): s`_i \in <<s>>%VS by rewrite memv_span ?memt_nth. have s_Zs a: \sum_(i < m) s`_i *~ a i \in <<s>>%VS. by rewrite memv_suml // => i _; rewrite -scaler_int memvZ. case s_v: (v \in <<s>>%VS); last by right=> [[a Dv]]; rewrite Dv s_Zs in s_v. pose IzT := {: 'I_m * 'I_(\dim <<s>>)}; pose Iz := 'I_#|IzT|. pose b := vbasis <<s>>. pose z_s := [seq coord b ij.2 (tnth s ij.1) | ij : IzT]. pose rank2 j i: Iz := enum_rank (i, j); pose val21 (p : Iz) := (enum_val p).1. pose inQzs w := [forall j, Crat_span z_s (coord b j w)]. have enum_pairK j: {in predT, cancel (rank2 j) val21}. by move=> i; rewrite /val21 enum_rankK. have Qz_Zs a: inQzs (\sum_(i < m) s`_i *~ a i). apply/forallP=> j; apply/Crat_spanP; rewrite /in_Crat_span size_map -cardE. exists [ffun ij => (a (val21 ij))%:Q *+ ((enum_val ij).2 == j)]. rewrite linear_sum {1}(reindex_onto _ _ (enum_pairK j)). rewrite big_mkcond; apply: eq_bigr => ij _ /=; rewrite nth_image (tnth_nth 0). rewrite (can2_eq (@enum_rankK _) (@enum_valK _)) ffunE -scaler_int /val21. case Dij: (enum_val ij) => [i j1]; rewrite xpair_eqE eqxx /= eq_sym -mulrb. by rewrite linearZ rmorphMn /= rmorph_int mulrnAl; case: eqP => // ->. case Qz_v: (inQzs v); last by right=> [[a Dv]]; rewrite Dv Qz_Zs in Qz_v. have [Qz [QzC [z1s Dz_s _]]] := num_field_exists z_s. have sz_z1s: size z1s = #|IzT| by rewrite -(size_map QzC) Dz_s size_map cardE. have xv j: {x | coord b j v = QzC x}. apply: sig_eqW; have /Crat_spanP[x ->] := forallP Qz_v j. exists (\sum_ij x ij *: z1s`_ij); rewrite rmorph_sum. apply: eq_bigr => ij _; rewrite mulrAC. apply: canLR (mulfK _) _; first by rewrite intr_eq0 denq_neq0. rewrite mulrzr -rmorphMz scalerMzl -(mulrzr (x _)) -numqE scaler_int. by rewrite rmorphMz mulrzl -(nth_map _ 0) ?Dz_s // -(size_map QzC) Dz_s. pose sz := [tuple [ffun j => z1s`_(rank2 j i)] | i < m]. have [Zsv | Zs'v] := dec_Qint_span sz [ffun j => sval (xv j)]. left; have{Zsv} [a Dv] := Zsv; exists a. transitivity (\sum_j \sum_(i < m) QzC ((sz`_i *~ a i) j) *: b`_j). rewrite {1}(coord_vbasis s_v) -/b; apply: eq_bigr => j _. rewrite -scaler_suml; congr (_ *: _). have{Dv} /ffunP/(_ j) := Dv; rewrite sum_ffunE !ffunE -rmorph_sum => <-. by case: (xv j). rewrite exchange_big; apply: eq_bigr => i _. rewrite (coord_vbasis (s_s i)) -/b mulrz_suml; apply: eq_bigr => j _. rewrite scalerMzl ffunMzE rmorphMz; congr ((_ *~ _) *: _). rewrite nth_mktuple ffunE -(nth_map _ 0) ?sz_z1s // Dz_s. by rewrite nth_image enum_rankK /= (tnth_nth 0). right=> [[a Dv]]; case: Zs'v; exists a. apply/ffunP=> j; rewrite sum_ffunE !ffunE; apply: (fmorph_inj QzC). case: (xv j) => /= _ <-; rewrite Dv linear_sum rmorph_sum /=. apply: eq_bigr => i _; rewrite nth_mktuple raddfMz !ffunMzE rmorphMz ffunE. by rewrite -(nth_map _ 0 QzC) ?sz_z1s // Dz_s nth_image enum_rankK -tnth_nth. 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)