proposition: Lemma dhomog_vecaxiom: vector_axiom 'C(d + n, d) (dhomog n.+1 R d).
proof: Proof. pose b := sbasis n.+1 d. pose t := [tuple of nseq d (0 : 'I_n.+1)]. pose M := fun i => nth 0%MM b i. pose f (p : dhomog n.+1 R d) := \row_(i < 'C(d + n, d)) p@_(nth 0%MM b i). exists f => /= [c p q|]. by apply/matrixP=> i j; rewrite !mxE /= mcoeffD mcoeffZ. pose g (r : 'rV[R]_('C(d + n, d))) : {mpoly R[_]} := \sum_(i < 'C(d + n, d)) (r 0 i) *: 'X_[M i]. have dhg r: g r \is d.-homog. rewrite rpred_sum //= => i _; apply/rpredZ. rewrite dhomogX basis_cover /M (nth_map t); last first. by rewrite -cardE card_sorted_tuples. by apply/map_f/mem_nth; rewrite -cardE card_sorted_tuples. exists (fun r => DHomog (dhg r)); last first. move=> r; rewrite /g /f /=; apply/matrixP=> i j. rewrite mxE ord1 raddf_sum /= -/(M _) (bigD1 j) //=. rewrite mcoeffZ mcoeffX eqxx mulr1 big1 ?addr0 //. move=> k ne_kj; rewrite mcoeffZ mcoeffX /M. rewrite nth_uniq ?size_basis ?uniq_basis //. by rewrite (inj_eq (val_inj)) (negbTE ne_kj) mulr0. move=> p; apply/val_inj/mpolyP=> m /=; rewrite /g /f. pose P := fun (p : {mpoly R[n.+1]}) m => p@_m *: 'X_[m]. rewrite (eq_bigr (P p \o M \o val)) /P /=; last first. by move=> /= i _; rewrite mxE. rewrite -(big_map (M \o val) xpredT (P p)) {}/P /M /=. rewrite /index_enum -enumT /= map_comp val_enum_ord. set r := map _ _; have {r}->: r = b; rewrite ?raddf_sum /=. apply/(@eq_from_nth _ 0%MM). by rewrite size_map size_iota size_basis. rewrite size_map size_iota=> i lt_i_C. by rewrite (nth_map 0%N) ?size_iota // nth_iota. case: (mdeg m =P d)=> /eqP; rewrite basis_cover -/b. move=> m_in_b; rewrite (bigD1_seq m) ?uniq_basis //=. rewrite mcoeffZ mcoeffX eqxx mulr1 big1 ?addr0 // => m' ne. by rewrite mcoeffZ mcoeffX (negbTE ne) mulr0. move=> m_notin_b; rewrite big_seq big1 /=. apply/esym/(@dhomog_nemf_coeff _ _ mdeg d). exact/dhomog_is_dhomog. by rewrite basis_cover. move=> m'; apply/contraTeq; rewrite mcoeffZ mcoeffX. by case: (m' =P m)=> [->|_]; last rewrite mulr0 eqxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(order fingroup perm ssralg zmodp poly ssrint) mathcomp(matrix vector) mathcomp(bigenough) ssrcomplements freeg