diff options
| author | Cyril Cohen | 2020-06-02 16:57:34 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2020-06-06 01:45:04 +0200 |
| commit | ccea59192ab383a9a0009d5ac5873e53f115c867 (patch) | |
| tree | 7e376f55fccf99a5a45b67ce346c9351c92ae3f0 /mathcomp/field | |
| parent | 7f355343ee30f72d8ab3ce87f897dc0092e43c29 (diff) | |
Improvements
- deprecating `fintype.arg_(min|max)P`
- removing dangling comments connecting min max and meet join
- better compatibility module
- removing broken notations with `\min` and `\max` (no neutral available)
- fixing `incompare` and `incomparel` in order.v
- adding missing elimination lemmas (`(comparable_)?(max|min)E[lg][et]`)
- adding missing `(comparable|real)_arg(min|max)P`
- CHANGELOG update
Diffstat (limited to 'mathcomp/field')
| -rw-r--r-- | mathcomp/field/finfield.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/field/finfield.v b/mathcomp/field/finfield.v index f0d432f..492aed8 100644 --- a/mathcomp/field/finfield.v +++ b/mathcomp/field/finfield.v @@ -506,7 +506,7 @@ have [r r_dv_p irr_r]: {r | r %| p & irreducible_poly r}. pose rVp (v : 'rV_n) (r := rVpoly v) := (1 < size r) && (r %| p). have [v0 Dp]: {v0 | rVpoly v0 = p & rVp v0}. by exists (poly_rV p); rewrite /rVp poly_rV_K ?C'p /=. - case/(arg_minP (size \o rVpoly))=> /= v; set r := rVpoly v. + case/(arg_minnP (size \o rVpoly))=> /= v; set r := rVpoly v. case/andP=> C'r r_dv_p min_r; exists r => //; split=> // q C'q q_dv_r. have nz_r: r != 0 by rewrite -size_poly_gt0 ltnW. have le_q_r: size q <= size r by rewrite dvdp_leq. |