proposition: Lemma BCH_det_mlinear t r' (f : 'I_r'.+1 -> 'I_n) (rt : r' < t.*2) : let B := \matrix_(i, j) BCH.PCM_alt a t (widen_ord rt i) (f j) in let V := Vandermonde r'.+1 (row 0 B) in \det B = \prod_(i < r'.+1) BCH.PCM_alt a t (widen_ord rt 0) (f i) * \det V.
proof: Proof. move=> B V. set h := Vandermonde r'.+1 (row 0 B). set g := fun i => BCH.PCM_alt a t (widen_ord (rt) 0) (f i). transitivity (\det (\matrix_(i, j) (h i j * g j))). congr (\det _). apply/matrixP => i j. by rewrite !mxE /h /g /BCH.PCM_alt !mxE -!exprD /= -exprM mul1n addn1. rewrite det_mlinear; congr (_ * _). congr (\det _); apply/matrixP => i j; by rewrite !mxE /h -exprM. 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