diff options
| author | Laurent Théry | 2020-09-04 12:14:00 +0200 |
|---|---|---|
| committer | GitHub | 2020-09-04 12:14:00 +0200 |
| commit | d693784678f8a1889fdc3731587f31dc7c9377ff (patch) | |
| tree | 413e131d444270f9d993437f13122e4aa5bc4277 /mathcomp/algebra/mxpoly.v | |
| parent | 495919767802fea4089594726d585c9b5305df21 (diff) | |
| parent | 667dd52bd039a96f896b81533b0aaafe98b9f8de (diff) | |
Merge pull request #572 from CohenCyril/reindex_omap
Lemmas reindex_omap and bigD1_ord
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. |