proposition: Lemma card_rV_wo_zeros p n : prime p -> (\sum_(x : 'rV['F_p]_n | [forall j, x ord0 j != 0%R]) 1)%N = p.-1 ^ n.
proof: Proof. move=> primep. destruct p as [|p'] => //; destruct p' as [|p'] => //. set p := p'.+2. transitivity (\sum_(x : {: n.-tuple 'I_p.-1}) 1)%N; last first. by rewrite sum1_card card_tuple card_ord. pose g : 'F_p -> 'I_p.-1 := fun x => inord (cast_ord (@card_Fp _ primep) (enum_rank x : 'I_#|'F_p|)).-1. pose g' : 'I_p.-1 -> 'F_p := fun x => enum_val (cast_ord (esym (@card_Fp _ primep)) (inord x.+1)). have Hg' : forall j, g' j != 0. move=> j; apply/eqP => /(congr1 enum_rank). rewrite enum_valK => /(congr1 val) /=. by rewrite enum_rank_ord /= inordK // ltnS. have gg' : {in [set x in 'F_p | x != 0], cancel g g'}. move=> x; rewrite inE => /andP[Hx x_neq0]. rewrite /g' inordK //=; last first. rewrite enum_rank_ord //= prednK ?lt0n //. move: (ltn_ord x) => /=; rewrite ltnS => /leq_trans; apply. by rewrite -(ltn_add2r 1) 2!addn1 Zp_cast // ?pdiv_leq // pdiv_id. rewrite (enum_rank_ord x) //= prednK ?lt0n //= enum_val_ord /=. apply val_inj => /=; rewrite inordK //. move: (ltn_ord x) => /leq_trans; apply; by rewrite Zp_cast ?pdiv_id. have g'g : cancel g' g. move=> x; rewrite /g /g' /= enum_valK; apply val_inj => /=. by rewrite (@inordK _ x.+1) /= ?inordK // ltnS. set f : 'rV['F_p]_n -> n.-tuple 'I_p.-1 := fun x => tuple_of_row (map_mx g x). set f' : n.-tuple 'I_p.-1 -> 'rV['F_p]_n := fun x => map_mx g' (row_of_tuple x). rewrite (reindex_onto f' f); last first. rewrite /= => x /forallP /= H; apply/rowP => j. by rewrite /f' /f mxE tuple_of_rowK mxE gg' // !inE /= H. apply eq_bigl => x; apply/andP; split. by apply/forallP => j; rewrite !mxE Hg'. apply/eqP/eq_from_tnth => i; by rewrite tnth_mktuple !mxE g'g. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) ssr_ext f2