From efed1800a4f2eaa942704ab8bebc60d9a3ac8dfd Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Sat, 30 May 2020 05:29:37 +0200
Subject: General theory of min and max, and use in ssrnum

- min and max can now be used in a partial order (sometimes under preconditions)
- min and max can now be used in a numDomainType (sometimes under preconditions)
---
 mathcomp/field/algebraics_fundamentals.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'mathcomp/field')

diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v
index 0a759e8..d8ad524 100644
--- a/mathcomp/field/algebraics_fundamentals.v
+++ b/mathcomp/field/algebraics_fundamentals.v
@@ -505,8 +505,8 @@ have add_Rroot xR p c: {yR | extendsR xR yR & has_Rroot xR p c -> root_in yR p}.
     have /(find_root r.1)[n ub_rp] := xab0; exists n.
     have [M Mgt0 ubM]: {M | 0 < M & {in Iab_ n, forall a, `|r.2.[a]| <= M}}.
       have [M ubM] := poly_itv_bound r.2 (ab_ n).1 (ab_ n).2.
-      exists (Num.max 1 M) => [|s /ubM vM]; first by rewrite ltxU ltr01.
-      by rewrite lexU orbC vM.
+      exists (Num.max 1 M) => [|s /ubM vM]; first by rewrite lt_maxr ltr01.
+      by rewrite le_maxr orbC vM.
     exists (h2 / M) => [|a xn_a]; first by rewrite divr_gt0 ?invr_gt0 ?ltr0n.
     rewrite ltr_pdivr_mulr // -(ltr_add2l h2) -mulr2n -mulr_natl divff //.
     rewrite -normr1 -(hornerC 1 a) -[1%:P]r_pq_1 hornerD.
-- 
cgit v1.2.3


From ccea59192ab383a9a0009d5ac5873e53f115c867 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Tue, 2 Jun 2020 16:57:34 +0200
Subject: 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
---
 mathcomp/field/finfield.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/field')

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.
-- 
cgit v1.2.3