diff options
Diffstat (limited to 'mathcomp/algebra')
| -rw-r--r-- | mathcomp/algebra/matrix.v | 27 | ||||
| -rw-r--r-- | mathcomp/algebra/mxpoly.v | 2 |
2 files changed, 13 insertions, 16 deletions
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index f32db72..e0ac874 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -1309,10 +1309,10 @@ Lemma matrix_sum_delta A : A = \sum_(i < m) \sum_(j < n) A i j *: delta_mx i j. Proof. apply/matrixP=> i j. -rewrite summxE (bigD1 i) // summxE (bigD1 j) //= !mxE !eqxx mulr1. -rewrite !big1 ?addr0 //= => [i' | j']; rewrite eq_sym => /negPf diff. - by rewrite summxE big1 // => j' _; rewrite !mxE diff mulr0. -by rewrite !mxE eqxx diff mulr0. +rewrite summxE (bigD1_ord i) // summxE (bigD1_ord j) //= !mxE !eqxx mulr1. +rewrite !big1 ?addr0 //= => [i' | j'] _. + by rewrite summxE big1// => j' _; rewrite !mxE eq_liftF mulr0. +by rewrite !mxE eqxx eq_liftF mulr0. Qed. End RingModule. @@ -1425,9 +1425,8 @@ Canonical diag_mx_linear n := Linear (@diag_mx_is_linear n). Lemma diag_mx_sum_delta n (d : 'rV_n) : diag_mx d = \sum_i d 0 i *: delta_mx i i. Proof. -apply/matrixP=> i j; rewrite summxE (bigD1 i) //= !mxE eqxx /=. -rewrite eq_sym mulr_natr big1 ?addr0 // => i' ne_i'i. -by rewrite !mxE eq_sym (negPf ne_i'i) mulr0. +apply/matrixP=> i j; rewrite summxE (bigD1_ord i) //= !mxE eqxx /=. +by rewrite eq_sym mulr_natr big1 ?addr0 // => i'; rewrite !mxE eq_liftF mulr0. Qed. Lemma row_diag_mx n (d : 'rV_n) i : @@ -1638,8 +1637,8 @@ Qed. Lemma rowE m n i (A : 'M_(m, n)) : row i A = delta_mx 0 i *m A. Proof. -apply/rowP=> j; rewrite !mxE (bigD1 i) //= mxE !eqxx mul1r. -by rewrite big1 ?addr0 // => i' ne_i'i; rewrite mxE /= (negPf ne_i'i) mul0r. +apply/rowP=> j; rewrite !mxE (bigD1_ord i) //= mxE !eqxx mul1r. +by rewrite big1 ?addr0 // => i'; rewrite mxE /= lift_eqF mul0r. Qed. Lemma row_mul m n p (i : 'I_m) A (B : 'M_(n, p)) : @@ -1655,9 +1654,9 @@ Qed. Lemma mul_delta_mx_cond m n p (j1 j2 : 'I_n) (i1 : 'I_m) (k2 : 'I_p) : delta_mx i1 j1 *m delta_mx j2 k2 = delta_mx i1 k2 *+ (j1 == j2). Proof. -apply/matrixP => i k; rewrite !mxE (bigD1 j1) //=. +apply/matrixP => i k; rewrite !mxE (bigD1_ord j1) //=. rewrite mulmxnE !mxE !eqxx andbT -natrM -mulrnA !mulnb !andbA andbAC. -by rewrite big1 ?addr0 // => j; rewrite !mxE andbC -natrM; move/negPf->. +by rewrite big1 ?addr0 // => j; rewrite !mxE andbC -natrM lift_eqF. Qed. Lemma mul_delta_mx m n p (j : 'I_n) (i : 'I_m) (k : 'I_p) : @@ -2844,10 +2843,8 @@ have{IHn} w_ j : exists w : 'rV_n.+1, [/\ w != 0, w 0 j = 0 & w *m A' = 0]. rewrite !mxE unlift_none -wjA'0; split=> //. apply: contraNneq nzwj => w0; apply/eqP/rowP=> k'. by move/rowP/(_ (lift j k')): w0; rewrite !mxE liftK. - apply/rowP=> k; rewrite !mxE (bigD1 j) //= mxE unlift_none mul0r add0r. - rewrite (reindex_onto (lift j) (odflt k \o unlift j)) /= => [|k']. - by apply: eq_big => k'; rewrite ?mxE liftK eq_sym neq_lift eqxx. - by rewrite eq_sym; case/unlift_some=> ? ? ->. + apply/rowP=> k; rewrite !mxE (bigD1_ord j) //= mxE unlift_none mul0r add0r. + by apply: eq_big => //= k'; rewrite !mxE/= liftK. have [w0 [/rV0Pn[j nz_w0j] w00_0 w0A']] := w_ 0; pose a0 := (w0 *m vA) 0 0. have{w_} [wj [nz_wj wj0_0 wjA']] := w_ j; pose aj := (wj *m vA) 0 0. have [aj0 | nz_aj] := eqVneq aj 0. diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v index cbac070..f33e291 100644 --- a/mathcomp/algebra/mxpoly.v +++ b/mathcomp/algebra/mxpoly.v @@ -188,7 +188,7 @@ have: rj0T (Ss_ dj.+1) = 'X^dj *: rj0T (S_ j1) + 1 *: rj0T (Ss_ dj). rewrite Sylvester_mxE insubdK; last exact: leq_ltn_trans (ltjS). by have [->|] := eqP; rewrite (addr0, add0r). rewrite -det_tr => /determinant_multilinear->; - try by apply/matrixP=> i j; rewrite !mxE eq_sym (negPf (neq_lift _ _)). + try by apply/matrixP=> i j; rewrite !mxE lift_eqF. have [dj0 | dj_gt0] := posnP dj; rewrite ?dj0 !mul1r. rewrite !det_tr det_map_mx addrC (expand_det_col _ j0) big1 => [|i _]. rewrite add0r; congr (\det _)%:P. |