diff options
| author | Cyril Cohen | 2020-09-01 15:44:13 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2020-09-03 19:59:28 +0200 |
| commit | fbeec199e65fe7e9fd96ddd74e31aa0461c22927 (patch) | |
| tree | bff3b089214e20c21a63b053670793a7bf44fe91 /mathcomp/algebra/mxpoly.v | |
| parent | 495919767802fea4089594726d585c9b5305df21 (diff) | |
Lemmas reindex_omap and bigD1_ord
+ eq_liftF and lift_eqF
+ proof simplificaions
Diffstat (limited to 'mathcomp/algebra/mxpoly.v')
| -rw-r--r-- | mathcomp/algebra/mxpoly.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |