proposition: Lemma rank_GRS_PCM_sq (b : 'rV_n) (rn : r <= n) (b0 : forall i, b ``_i != 0) : \rank (GRS_PCM_sq a b r) = r.
proof: Proof. apply mxrank_unit. rewrite unitmxE unitfE GRS_PCM_sq_vander // det_mulmx mulf_neq0 //; last first. by rewrite det_diag prodf_seq_neq0; apply/allP => /= i _; rewrite mxE b0. case: r rn => [|r' rn]; first by rewrite det_mx00 oner_neq0. rewrite vandermonde.det_Vandermonde prodf_seq_neq0; apply/allP => /= i _. rewrite prodf_seq_neq0; apply/allP => /= j _; apply/implyP. rewrite ltnNge => ij; rewrite !mxE subr_eq0; apply: contra ij => /eqP ij. move: (@a_inj (inord i) (inord j)); rewrite !ffunE ij => /(_ erefl). move/(congr1 (@nat_of_ord n)). rewrite inordK // ?(leq_trans (ltn_ord i)) // => ->. by rewrite inordK // (leq_trans (ltn_ord j)). Qed.
imports: mathcomp(all_ssreflect ssralg finalg poly polydiv cyclic) mathcomp(perm matrix mxpoly vector mxalgebra zmodp) ssr_ext ssralg_ext vandermonde linearcode dft poly_decoding