diff options
Diffstat (limited to 'mathcomp/algebra')
| -rw-r--r-- | mathcomp/algebra/intdiv.v | 2 | ||||
| -rw-r--r-- | mathcomp/algebra/mxalgebra.v | 21 | ||||
| -rw-r--r-- | mathcomp/algebra/mxpoly.v | 10 | ||||
| -rw-r--r-- | mathcomp/algebra/poly.v | 30 | ||||
| -rw-r--r-- | mathcomp/algebra/polyXY.v | 2 | ||||
| -rw-r--r-- | mathcomp/algebra/polydiv.v | 81 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 7 |
7 files changed, 72 insertions, 81 deletions
diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v index 122457d..7663e63 100644 --- a/mathcomp/algebra/intdiv.v +++ b/mathcomp/algebra/intdiv.v @@ -909,7 +909,7 @@ wlog Dj: j M nzMij / j = 0; last rewrite {j}Dj in nzMij. by rewrite xcolE unitmx_mul uR unitmx_perm. by rewrite xcolE !mulmxA -dM xcolE -mulmxA -perm_mxM tperm2 perm_mx1 mulmx1. move Da: (M i 0) nzMij => a nz_a. -elim: {a}_.+1 {-2}a (ltnSn `|a|) => // A IHa a leA in m n M i Da nz_a le_mn *. +have [A leA] := ubnP `|a|; elim: A => // A IHa in a leA m n M i Da nz_a le_mn *. wlog [j a'Mij]: m n M i Da le_mn / {j | ~~ (a %| M i j)%Z}; last first. have nz_j: j != 0 by apply: contraNneq a'Mij => ->; rewrite Da. case: n => [[[]//]|n] in j le_mn nz_j M a'Mij Da *. diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v index a39aba1..38beffc 100644 --- a/mathcomp/algebra/mxalgebra.v +++ b/mathcomp/algebra/mxalgebra.v @@ -877,9 +877,9 @@ Lemma mxrank_leqif_sup m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : Proof. move=> sAB; split; first by rewrite mxrankS. apply/idP/idP=> [| sBA]; last by rewrite eqn_leq !mxrankS. -case/submxP: sAB => D ->; rewrite -{-2}(mulmx_base B) mulmxA. +case/submxP: sAB => D ->; set r := \rank B; rewrite -(mulmx_base B) mulmxA. rewrite mxrankMfree // => /row_fullP[E kE]. -by rewrite -{1}[row_base B]mul1mx -kE -(mulmxA E) (mulmxA _ E) submxMl. +by rewrite -[rB in _ *m rB]mul1mx -kE -(mulmxA E) (mulmxA _ E) submxMl. Qed. Lemma mxrank_leqif_eq m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : @@ -1100,7 +1100,7 @@ Lemma sub_sumsmxP P m n (A : 'M_(m, n)) (B_ : I -> 'M_n) : Proof. apply: (iffP idP) => [| [u_ ->]]; last first. by apply: summx_sub_sums => i _; apply: submxMl. -elim: {P}_.+1 {-2}P A (ltnSn #|P|) => // b IHb P A. +have [b] := ubnP #|P|; elim: b => // b IHb in P A *. case: (pickP P) => [i Pi | P0 _]; last first. rewrite big_pred0 //; move/submx0null->. by exists (fun _ => 0); rewrite big_pred0. @@ -1579,7 +1579,9 @@ Qed. Lemma proj_mx_proj n (U V : 'M_n) : let P := proj_mx U V in (U :&: V = 0)%MS -> P *m P = P. -Proof. by move=> P dxUV; rewrite -{-2}[P]mul1mx proj_mx_id ?proj_mx_sub. Qed. +Proof. +by move=> P dxUV; rewrite -[P in P *m _]mul1mx proj_mx_id ?proj_mx_sub ?mul1mx. +Qed. (* Completing a partially injective matrix to get a unit matrix. *) @@ -1845,7 +1847,8 @@ rewrite /TIsum; apply: (iffP eqnP) => /= [dxS i Pi | dxS]. set Si' := (\sum_(j | _) unwrap (S_ j))%MS. have: mxdirect (unwrap (S_ i) + Si') by apply/eqnP; rewrite /= -!(bigD1 i). by rewrite mxdirect_addsE => /and3P[-> _ /eqP]. -elim: _.+1 {-2 4}P (subxx P) (ltnSn #|P|) => // m IHm Q; move/subsetP=> sQP. +set Q := P; have [m] := ubnP #|Q|; have: Q \subset P by []. +elim: m Q => // m IHm Q /subsetP-sQP. case: (pickP Q) => [i Qi | Q0]; last by rewrite !big_pred0 ?mxrank0. rewrite (cardD1x Qi) !((bigD1 i) Q) //=. move/IHm=> <- {IHm}/=; last by apply/subsetP=> j /andP[/sQP]. @@ -1946,7 +1949,7 @@ Proof. by apply: (iffP (rowV0Pn _)) => [] [v]; move/eigenspaceP; exists v. Qed. Lemma mxdirect_sum_eigenspace (P : pred I) a_ : {in P &, injective a_} -> mxdirect (\sum_(i | P i) eigenspace (a_ i)). Proof. -elim: {P}_.+1 {-2}P (ltnSn #|P|) => // m IHm P lePm inj_a. +have [m] := ubnP #|P|; elim: m P => // m IHm P lePm inj_a. apply/mxdirect_sumsP=> i Pi; apply/eqP/rowV0P => v. rewrite sub_capmx => /andP[/eigenspaceP def_vg]. set Vi' := (\sum_(i | _) _)%MS => Vi'v. @@ -2109,9 +2112,9 @@ Proof. case: n => // n' _; set n := n'.+1; set p := #|F|. rewrite big_nat_rev big_add1 -triangular_sum expn_sum -big_split /=. pose fr m := [pred A : 'M[F]_(m, n) | \rank A == m]. -set m := {-7}n; transitivity #|fr m|. +set m := n; rewrite [in m.+1]/m; transitivity #|fr m|. by rewrite cardsT /= card_sub; apply: eq_card => A; rewrite -row_free_unit. -elim: m (leqnn m : m <= n) => [_|m IHm]; last move/ltnW=> le_mn. +have: m <= n by []; elim: m => [_ | m IHm /ltnW-le_mn]. rewrite (@eq_card1 _ (0 : 'M_(0, n))) ?big_geq //= => A. by rewrite flatmx0 !inE !eqxx. rewrite big_nat_recr // -{}IHm //= !subSS mulnBr muln1 -expnD subnKC //. @@ -2453,7 +2456,7 @@ Definition cent_mx_fun (B : 'M[F]_n) := R *m lin_mx (mulmxr B \- mulmx B). Lemma cent_mx_fun_is_linear : linear cent_mx_fun. Proof. move=> a A B; apply/row_matrixP=> i; rewrite linearP row_mul mul_rV_lin. -rewrite /= {-3}[row]lock row_mul mul_rV_lin -lock row_mul mul_rV_lin. +rewrite /= [row i _ as v in a *: v]row_mul mul_rV_lin row_mul mul_rV_lin. by rewrite -linearP -(linearP [linear of mulmx _ \- mulmxr _]). Qed. Canonical cent_mx_fun_additive := Additive cent_mx_fun_is_linear. diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v index b95933e..861a7df 100644 --- a/mathcomp/algebra/mxpoly.v +++ b/mathcomp/algebra/mxpoly.v @@ -179,13 +179,13 @@ have{Ss u} ->: Ss = Ss_ dS. by rewrite ltn_subRL (leq_trans _ k_ge_dS) // addnC ltn_add2l. by rewrite insubdK //; case: (split i) => {i}i; rewrite !mxE coefMXn; case: leqP. -elim: {-2}dS (leqnn dS) (dS_gt0) => // dj IHj dj_lt_dS _. -pose j1 := Ordinal dj_lt_dS; pose rj0T (A : 'M[{poly R}]_dS) := row j0 A^T. +case: (ubnPgeq dS) (dS_gt0); elim=> // dj IHj ltjS _; pose j1 := Ordinal ltjS. +pose rj0T (A : 'M[{poly R}]_dS) := row j0 A^T. have: rj0T (Ss_ dj.+1) = 'X^dj *: rj0T (S_ j1) + 1 *: rj0T (Ss_ dj). apply/rowP=> i; apply/polyP=> k; rewrite scale1r !(Sylvester_mxE, mxE) eqxx. rewrite coefD coefXnM coefC !coef_poly ltnS subn_eq0 ltn_neqAle andbC. case: (leqP k dj) => [k_le_dj | k_gt_dj] /=; last by rewrite addr0. - rewrite Sylvester_mxE insubdK; last exact: leq_ltn_trans (dj_lt_dS). + rewrite Sylvester_mxE insubdK; last exact: leq_ltn_trans (ltjS). by case: eqP => [-> | _]; rewrite (addr0, add0r). rewrite -det_tr => /determinant_multilinear->; try by apply/matrixP=> i j; rewrite !mxE eq_sym (negPf (neq_lift _ _)). @@ -858,8 +858,8 @@ have{mon_p pw0 intRp intRq}: genI S. split; set S1 := _ ++ _; first exists p. split=> // i; rewrite -[p]coefK coef_poly; case: ifP => // lt_i_p. by apply: genS; rewrite mem_cat orbC mem_nth. - have: all (mem S1) S1 by apply/allP. - elim: {-1}S1 => //= y S2 IH /andP[S1y S12]; split; last exact: IH. + set S2 := S1; have: all (mem S1) S2 by apply/allP. + elim: S2 => //= y S2 IH /andP[S1y S12]; split; last exact: IH. have{q S S1 IH S1y S12 intRp intRq} [q mon_q qx0]: integralOver RtoK y. by move: S1y; rewrite mem_cat => /orP[]; [apply: intRq | apply: intRp]. exists (map_poly RtoK q); split=> // [|i]; first exact: monic_map. diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v index eb96da2..2bb3614 100644 --- a/mathcomp/algebra/poly.v +++ b/mathcomp/algebra/poly.v @@ -1172,14 +1172,14 @@ Qed. Lemma multiplicity_XsubC p a : {m | exists2 q, (p != 0) ==> ~~ root q a & p = q * ('X - a%:P) ^+ m}. Proof. -elim: {p}(size p) {-2}p (eqxx (size p)) => [|n IHn] p. - by rewrite size_poly_eq0 => ->; exists 0%N, p; rewrite ?mulr1. -have [/sig_eqW[{p}p ->] sz_p | nz_pa] := altP (factor_theorem p a); last first. - by exists 0%N, p; rewrite ?mulr1 ?nz_pa ?implybT. -have nz_p: p != 0 by apply: contraTneq sz_p => ->; rewrite mul0r size_poly0. -rewrite size_Mmonic ?monicXsubC // size_XsubC addn2 eqSS in sz_p. -have [m /sig2_eqW[q nz_qa Dp]] := IHn p sz_p; rewrite nz_p /= in nz_qa. -by exists m.+1, q; rewrite ?nz_qa ?implybT // exprSr mulrA -Dp. +have [n le_p_n] := ubnP (size p); elim: n => // n IHn in p le_p_n *. +have [-> | nz_p /=] := eqVneq p 0; first by exists 0%N, 0; rewrite ?mul0r. +have [/sig_eqW[p1 Dp] | nz_pa] := altP (factor_theorem p a); last first. + by exists 0%N, p; rewrite ?mulr1. +have nz_p1: p1 != 0 by apply: contraNneq nz_p => p1_0; rewrite Dp p1_0 mul0r. +have /IHn[m /sig2_eqW[q nz_qa Dp1]]: size p1 < n. + by rewrite Dp size_Mmonic ?monicXsubC // size_XsubC addn2 in le_p_n. +by exists m.+1, q; [rewrite nz_p1 in nz_qa | rewrite exprSr mulrA -Dp1]. Qed. (* Roots of unity. *) @@ -2691,17 +2691,15 @@ Proof. pose polyT (p : seq F) := (foldr (fun c f => f * 'X_0 + c%:T) (0%R)%:T p)%T. have eval_polyT (q : {poly F}) x : GRing.eval [:: x] (polyT q) = q.[x]. by rewrite /horner; elim: (val q) => //= ? ? ->. -elim: size {-2}p (leqnn (size p)) => {p} [p|n IHn p]. - by move=> /size_poly_leq0P->; exists [::], 0; rewrite mul0r eqxx. +have [n] := ubnP (size p); elim: n => // n IHn in p *. have /decPcases /= := @satP F [::] ('exists 'X_0, polyT p == 0%T). case: ifP => [_ /sig_eqW[x]|_ noroot]; last first. exists [::], p; rewrite big_nil mulr1; split => // p_neq0 x. by apply/negP=> /rootP rpx; apply noroot; exists x; rewrite eval_polyT. -rewrite eval_polyT => /rootP /factor_theorem /sig_eqW [q ->]. -have [->|q_neq0] := eqVneq q 0; first by exists [::], 0; rewrite !mul0r eqxx. -rewrite size_mul ?polyXsubC_eq0 // ?size_XsubC addn2 /= ltnS => sq_le_n. -have [] // := IHn q => s [r [-> nr]]; exists (s ++ [::x]), r. -by rewrite big_cat /= big_seq1 mulrA. +rewrite eval_polyT => /rootP/factor_theorem/sig_eqW[p1 ->]. +have [->|nz_p1] := eqVneq p1 0; first by exists [::], 0; rewrite !mul0r eqxx. +rewrite size_Mmonic ?monicXsubC // size_XsubC addn2 => /IHn[s [q [-> irr_q]]]. +by exists (rcons s x), q; rewrite -cats1 big_cat big_seq1 mulrA. Qed. End DecField. @@ -2717,7 +2715,7 @@ Lemma closed_rootP p : reflect (exists x, root p x) (size p != 1%N). Proof. have [-> | nz_p] := eqVneq p 0. by rewrite size_poly0; left; exists 0; rewrite root0. -rewrite neq_ltn {1}polySpred //=. +rewrite neq_ltn [in _ < 1]polySpred //=. apply: (iffP idP) => [p_gt1 | [a]]; last exact: root_size_gt1. pose n := (size p).-1; have n_gt0: n > 0 by rewrite -ltnS -polySpred. have [a Dan] := closedF (fun i => - p`_i / lead_coef p) n_gt0. diff --git a/mathcomp/algebra/polyXY.v b/mathcomp/algebra/polyXY.v index e91b8be..9bc8fd5 100644 --- a/mathcomp/algebra/polyXY.v +++ b/mathcomp/algebra/polyXY.v @@ -374,7 +374,7 @@ move=> nz_px [q nz_q qx0]. have [/size1_polyC Dp | p_gt1] := leqP (size p) 1. by rewrite {}/pEx Dp map_polyC hornerC map_poly_eq0 in nz_px *; exists p`_0. have nz_p: p != 0 by rewrite -size_poly_gt0 ltnW. -elim: {q}_.+1 {-2}q (ltnSn (size q)) => // m IHm q le_qm in nz_q qx0 *. +have [m le_qm] := ubnP (size q); elim: m => // m IHm in q le_qm nz_q qx0 *. have nz_q1: q^:P != 0 by rewrite map_poly_eq0. have sz_q1: size q^:P = size q by rewrite size_map_polyC. have q1_gt1: size q^:P > 1. diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v index aa076a2..6b5d003 100644 --- a/mathcomp/algebra/polydiv.v +++ b/mathcomp/algebra/polydiv.v @@ -1728,18 +1728,16 @@ Proof. by move=> p; rewrite gcdpE ltnn modpp gcd0p. Qed. Lemma dvdp_gcdlr p q : (gcdp p q %| p) && (gcdp p q %| q). Proof. -elim: {p q}minn {-2}p {-2}q (leqnn (minn (size q) (size p))) => [|r Hrec] p q. - rewrite geq_min !leqn0 !size_poly_eq0. - by case/pred2P=> ->; rewrite (gcdp0, gcd0p) dvdpp ?andbT /=. -case: (eqVneq p 0) => [-> _|nz_p]; first by rewrite gcd0p dvdpp andbT. -case: (eqVneq q 0) => [->|nz_q]; first by rewrite gcdp0 dvdpp /=. -rewrite gcdpE minnC /minn; case: ltnP => [lt_pq | le_pq] le_qr. - suffices: minn (size p) (size (q %% p)) <= r. - by move/Hrec; case/andP => E1 E2; rewrite E2 (dvdp_mod _ E2). - by rewrite geq_min orbC -ltnS (leq_trans _ le_qr) ?ltn_modp. -suffices: minn (size q) (size (p %% q)) <= r. - by move/Hrec; case/andP => E1 E2; rewrite E2 andbT (dvdp_mod _ E2). -by rewrite geq_min orbC -ltnS (leq_trans _ le_qr) ?ltn_modp. +have [r] := ubnP (minn (size q) (size p)); elim: r => // r IHr in p q *. +have [-> | nz_p] := eqVneq p 0; first by rewrite gcd0p dvdpp andbT. +have [-> | nz_q] := eqVneq q 0; first by rewrite gcdp0 dvdpp /=. +rewrite ltnS gcdpE minnC /minn; case: ltnP => [lt_pq | le_pq] le_qr. + suffices /IHr/andP[E1 E2]: minn (size p) (size (q %% p)) < r. + by rewrite E2 (dvdp_mod _ E2). + by rewrite gtn_min orbC (leq_trans _ le_qr) ?ltn_modp. +suffices /IHr/andP[E1 E2]: minn (size q) (size (p %% q)) < r. + by rewrite E2 andbT (dvdp_mod _ E2). +by rewrite gtn_min orbC (leq_trans _ le_qr) ?ltn_modp. Qed. Lemma dvdp_gcdl p q : gcdp p q %| p. @@ -1756,22 +1754,18 @@ Proof. by move=> qn0; move: (dvdp_gcdr p q); apply: dvdp_leq. Qed. Lemma dvdp_gcd p m n : p %| gcdp m n = (p %| m) && (p %| n). Proof. -apply/idP/andP=> [dv_pmn | [dv_pm dv_pn]]. +apply/idP/andP=> [dv_pmn | []]. by rewrite ?(dvdp_trans dv_pmn) ?dvdp_gcdl ?dvdp_gcdr. -move: (leqnn (minn (size n) (size m))) dv_pm dv_pn. -elim: {m n}minn {-2}m {-2}n => [|r Hrec] m n. - rewrite geq_min !leqn0 !size_poly_eq0. - by case/pred2P=> ->; rewrite (gcdp0, gcd0p). -case: (eqVneq m 0) => [-> _|nz_m]; first by rewrite gcd0p /=. -case: (eqVneq n 0) => [->|nz_n]; first by rewrite gcdp0 /=. -rewrite gcdpE minnC /minn; case: ltnP => Cnm le_r dv_m dv_n. - apply: Hrec => //; last by rewrite -(dvdp_mod _ dv_m). - by rewrite geq_min orbC -ltnS (leq_trans _ le_r) ?ltn_modp. -apply: Hrec => //; last by rewrite -(dvdp_mod _ dv_n). -by rewrite geq_min orbC -ltnS (leq_trans _ le_r) ?ltn_modp. +have [r] := ubnP (minn (size n) (size m)); elim: r => // r IHr in m n *. +have [-> | nz_m] := eqVneq m 0; first by rewrite gcd0p. +have [-> | nz_n] := eqVneq n 0; first by rewrite gcdp0. +rewrite gcdpE minnC ltnS /minn; case: ltnP => [lt_mn | le_nm] le_r dv_m dv_n. + apply: IHr => //; last by rewrite -(dvdp_mod _ dv_m). + by rewrite gtn_min orbC (leq_trans _ le_r) ?ltn_modp. +apply: IHr => //; last by rewrite -(dvdp_mod _ dv_n). +by rewrite gtn_min orbC (leq_trans _ le_r) ?ltn_modp. Qed. - Lemma gcdpC : forall p q, gcdp p q %= gcdp q p. Proof. by move=> p q; rewrite /eqp !dvdp_gcd !dvdp_gcdl !dvdp_gcdr. Qed. @@ -3233,24 +3227,19 @@ Qed. Lemma dvdp_gdcor p q : q != 0 -> p %| (gdcop q p) * (q ^+ size p). Proof. -move=> q_neq0; rewrite /gdcop. -elim: (size p) {-2 5}p (leqnn (size p))=> {p} [|n ihn] p. - rewrite size_poly_leq0; move/eqP->. - by rewrite size_poly0 /= dvd0p expr0 mulr1 (negPf q_neq0). -move=> hsp /=; have [->|p_neq0] := altP (p =P 0). - rewrite size_poly0 /= dvd0p expr0 mulr1 div0p /=. - case: ifP=> // _; have := (ihn 0). - by rewrite size_poly0 expr0 mulr1 dvd0p=> /(_ isT). -have [|ncop_pq] := boolP (coprimep _ _); first by rewrite dvdp_mulr ?dvdpp. -have g_gt1: (1 < size (gcdp p q))%N. - have [//||/esym/eqP] := ltngtP; last by rewrite -coprimep_def (negPf ncop_pq). - by rewrite ltnS leqn0 size_poly_eq0 gcdp_eq0 (negPf p_neq0). -have sd : (size (p %/ gcdp p q) < size p)%N. +rewrite /gdcop => nz_q; have [n hsp] := ubnPleq (size p). +elim: n => [|n IHn] /= in p hsp *; first by rewrite (negPf nz_q) mul0r dvdp0. +have [_ | ncop_pq] := ifPn; first by rewrite dvdp_mulr. +have g_gt1: 1 < size (gcdp p q). + rewrite ltn_neqAle eq_sym ncop_pq lt0n size_poly_eq0 gcdp_eq0. + by rewrite negb_and nz_q orbT. +have [-> | nz_p] := eqVneq p 0. + by rewrite div0p exprSr mulrA dvdp_mulr // IHn // size_poly0. +have le_d_p: size (p %/ gcdp p q) < size p. rewrite size_divp -?size_poly_eq0 -(subnKC g_gt1) // add2n /=. - by rewrite -[size _]prednK ?size_poly_gt0 // ltnS subSS leq_subr. -rewrite -{1}[p](divpK (dvdp_gcdl _ q)) -(subnKC sd) addSnnS exprD mulrA. -rewrite dvdp_mul ?ihn //; first by rewrite -ltnS (leq_trans sd). -by rewrite exprS dvdp_mulr // dvdp_gcdr. + by rewrite polySpred // ltnS subSS leq_subr. +rewrite -[p in p %| _](divpK (dvdp_gcdl p q)) exprSr mulrA. +by rewrite dvdp_mul ?IHn ?dvdp_gcdr // -ltnS (leq_trans le_d_p). Qed. Lemma reducible_cubic_root p q : @@ -3291,8 +3280,8 @@ Lemma redivp_map a b : redivp a^f b^f = (rscalp a b, (rdivp a b)^f, (rmodp a b)^f). Proof. rewrite /rdivp /rscalp /rmodp !unlock map_poly_eq0 size_map_poly. -case: eqP; rewrite /= -(rmorph0 (map_poly_rmorphism f)) //; move/eqP=> q_nz. -move: (size a) => m; elim: m 0%N 0 a => [|m IHm] qq r a /=. +have [// | q_nz] := ifPn; rewrite -(rmorph0 (map_poly_rmorphism f)) //. +have [m _] := ubnPeq (size a); elim: m 0%N 0 a => [|m IHm] qq r a /=. rewrite -!mul_polyC !size_map_poly !lead_coef_map // -(map_polyXn f). by rewrite -!(map_polyC f) -!rmorphM -rmorphB -rmorphD; case: (_ < _). rewrite -!mul_polyC !size_map_poly !lead_coef_map // -(map_polyXn f). @@ -3359,9 +3348,9 @@ wlog lt_p_q: p q / size p < size q. rewrite gcdpE (gcdpE p^f) !size_map_poly ltnNge le_q_p /= -map_modp. case: (eqVneq q 0) => [-> | q_nz]; first by rewrite rmorph0 !gcdp0. by rewrite IHpq ?ltn_modp. -elim: {q}_.+1 p {-2}q (ltnSn (size q)) lt_p_q => // m IHm p q le_q_m lt_p_q. +have [m le_q_m] := ubnP (size q); elim: m => // m IHm in p q lt_p_q le_q_m *. rewrite gcdpE (gcdpE p^f) !size_map_poly lt_p_q -map_modp. -case: (eqVneq p 0) => [-> | q_nz]; first by rewrite rmorph0 !gcdp0. +have [-> | q_nz] := eqVneq p 0; first by rewrite rmorph0 !gcdp0. by rewrite IHm ?(leq_trans lt_p_q) ?ltn_modp. Qed. diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index f8c5675..495ce18 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -3185,7 +3185,7 @@ Lemma lerif_AGM_scaled (I : finType) (A : {pred I}) (E : I -> R) (n := #|A|) : \prod_(i in A) (E i *+ n) <= (\sum_(i in A) E i) ^+ n ?= iff [forall i in A, forall j in A, E i == E j]. Proof. -elim: {A}_.+1 {-2}A (ltnSn #|A|) => // m IHm A leAm in E n * => Ege0. +have [m leAm] := ubnP #|A|; elim: m => // m IHm in A leAm E n * => Ege0. apply/lerifP; case: ifPn => [/forall_inP-Econstant | Enonconstant]. have [i /= Ai | A0] := pickP (mem A); last by rewrite [n]eq_card0 ?big_pred0. have /eqfun_inP-E_i := Econstant i Ai; rewrite -(eq_bigr _ E_i) sumr_const. @@ -4990,8 +4990,9 @@ Qed. Lemma normC_sub_eq x y : `|x - y| = `|x| - `|y| -> {t | `|t| == 1 & (x, y) = (`|x| * t, `|y| * t)}. Proof. -rewrite -{-1}(subrK y x) => /(canLR (subrK _))/esym-Dx; rewrite Dx. -by have [t ? [Dxy Dy]] := normC_add_eq Dx; exists t; rewrite // mulrDl -Dxy -Dy. +set z := x - y; rewrite -(subrK y x) -/z => /(canLR (subrK _))/esym-Dx. +have [t t_1 [Dz Dy]] := normC_add_eq Dx. +by exists t; rewrite // Dx mulrDl -Dz -Dy. Qed. End ClosedFieldTheory. |