proposition: Lemma det_B_neq0 t r f (Hr' : r.+1 < t.*2) (Hinj : injective f) : let B := \matrix_(i < r.+1, j < r.+1) BCH.PCM_alt a t (widen_ord (ltnW Hr') i) (f j) in \det B != 0.
proof: Proof. rewrite /=; set B := \matrix_(_, _) _. rewrite BCH_det_mlinear det_Vandermonde mulf_neq0 //. - rewrite prodf_seq_neq0 /=; apply/allP => /= j _. by rewrite !mxE /= expr1 (proj2 a_neq0). - rewrite prodf_seq_neq0 /=; apply/allP => /= j _. rewrite prodf_seq_neq0 /=; apply/allP => /= k _. apply/implyP => jk; rewrite !mxE /= !expr1 subr_eq0. apply/negP => /eqP; move: (proj1 a_neq0) => /(_ (f k) (f j)). by rewrite 2!ffunE => akj /akj/Hinj; exact/eqP/negbT/gtn_eqF. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv finalg zmodp) mathcomp(matrix mxalgebra mxpoly vector fieldext finfield) ssralg_ext hamming linearcode decoding cyclic_code poly_decoding vandermonde dft euclid grs f2