diff options
Diffstat (limited to 'mathcomp')
39 files changed, 482 insertions, 320 deletions
diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v index 808d21d..336b6df 100644 --- a/mathcomp/algebra/intdiv.v +++ b/mathcomp/algebra/intdiv.v @@ -601,11 +601,11 @@ Proof. by rewrite /gcdz abszM => /Gauss_gcdr->. Qed. Lemma Gauss_gcdzl p m n : coprimez p n -> gcdz p (m * n) = gcdz p m. Proof. by move=> co_pn; rewrite mulrC Gauss_gcdzr. Qed. -Lemma coprimez_mulr p m n : coprimez p (m * n) = coprimez p m && coprimez p n. -Proof. by rewrite -coprime_mulr -abszM. Qed. +Lemma coprimezMr p m n : coprimez p (m * n) = coprimez p m && coprimez p n. +Proof. by rewrite -coprimeMr -abszM. Qed. -Lemma coprimez_mull p m n : coprimez (m * n) p = coprimez m p && coprimez n p. -Proof. by rewrite -coprime_mull -abszM. Qed. +Lemma coprimezMl p m n : coprimez (m * n) p = coprimez m p && coprimez n p. +Proof. by rewrite -coprimeMl -abszM. Qed. Lemma coprimez_pexpl k m n : (0 < k)%N -> coprimez (m ^+ k) n = coprimez m n. Proof. by rewrite /coprimez /gcdz abszX; apply: coprime_pexpl. Qed. @@ -613,11 +613,11 @@ Proof. by rewrite /coprimez /gcdz abszX; apply: coprime_pexpl. Qed. Lemma coprimez_pexpr k m n : (0 < k)%N -> coprimez m (n ^+ k) = coprimez m n. Proof. by move=> k_gt0; rewrite !(coprimez_sym m) coprimez_pexpl. Qed. -Lemma coprimez_expl k m n : coprimez m n -> coprimez (m ^+ k) n. -Proof. by rewrite /coprimez /gcdz abszX; apply: coprime_expl. Qed. +Lemma coprimezXl k m n : coprimez m n -> coprimez (m ^+ k) n. +Proof. by rewrite /coprimez /gcdz abszX; apply: coprimeXl. Qed. -Lemma coprimez_expr k m n : coprimez m n -> coprimez m (n ^+ k). -Proof. by rewrite !(coprimez_sym m); apply: coprimez_expl. Qed. +Lemma coprimezXr k m n : coprimez m n -> coprimez m (n ^+ k). +Proof. by rewrite !(coprimez_sym m); apply: coprimezXl. Qed. Lemma coprimez_dvdl m n p : (m %| n)%N -> coprimez n p -> coprimez m p. Proof. exact: coprime_dvdl. Qed. @@ -878,7 +878,7 @@ Lemma dvdpP_rat_int p q : {p1 : {poly int} & {a | a != 0 & p = a *: pZtoQ p1} & {r | q = p1 * r}}. Proof. have{p} [p [a nz_a ->]] := rat_poly_scale p. -rewrite dvdp_scalel ?invr_eq0 ?intr_eq0 // dvdp_rat_int => dv_p_q. +rewrite dvdpZl ?invr_eq0 ?intr_eq0 // dvdp_rat_int => dv_p_q. exists (zprimitive p); last exact: dvdpP_int. have [-> | nz_p] := eqVneq p 0. by exists 1; rewrite ?oner_eq0 // zprimitive0 map_poly0 !scaler0. @@ -1074,3 +1074,12 @@ rewrite -defS -2!mulmxA; have ->: T *m pinvmx T = 1%:M. by apply: (row_free_inj uT); rewrite mul1mx mulmxKpV. by move=> i; rewrite mulmx1 -map_mxM 2!mxE denq_int mxE. Qed. + +Notation "@ 'coprimez_expl'" := + (deprecate coprimez_expl coprimezXl) (at level 10, only parsing) : fun_scope. +Notation "@ 'coprimez_expr'" := + (deprecate coprimez_expr coprimezXr) (at level 10, only parsing) : fun_scope. +Notation coprimez_mull := (deprecate coprimez_mull coprimezMl) (only parsing). +Notation coprimez_mulr := (deprecate coprimez_mulr coprimezMr) (only parsing). +Notation coprimez_expl := (fun k => @coprimez_expl k _ _) (only parsing). +Notation coprimez_expr := (fun k => @coprimez_expr k _ _) (only parsing). diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index feb9edd..f7d7730 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -1699,12 +1699,12 @@ Proof. by apply/matrixP=> i j; rewrite !mxE raddfN. Qed. Lemma map_mxD A B : (A + B)^f = A^f + B^f. Proof. by apply/matrixP=> i j; rewrite !mxE raddfD. Qed. -Lemma map_mx_sub A B : (A - B)^f = A^f - B^f. +Lemma map_mxB A B : (A - B)^f = A^f - B^f. Proof. by rewrite map_mxD map_mxN. Qed. Definition map_mx_sum := big_morph _ map_mxD map_mx0. -Canonical map_mx_additive := Additive map_mx_sub. +Canonical map_mx_additive := Additive map_mxB. End MapZmodMatrix. @@ -2691,7 +2691,7 @@ Proof. by apply/matrixP=> i j; rewrite !mxE cofactor_map_mx. Qed. End FixedSize. Lemma map_copid_mx n r : (copid_mx r)^f = copid_mx r :> 'M_n. -Proof. by rewrite map_mx_sub map_mx1 map_pid_mx. Qed. +Proof. by rewrite map_mxB map_mx1 map_pid_mx. Qed. Lemma map_mx_is_multiplicative n' (n := n'.+1) : multiplicative (map_mx f : 'M_n -> 'M_n). @@ -3687,3 +3687,7 @@ Canonical mxOver_subringPred (S : {pred R}) (ringS : subringPred S) End mxRingOver. End mxOver. + +Notation "@ 'map_mx_sub'" := + (deprecate map_mx_sub map_mxB) (at level 10, only parsing) : fun_scope. +Notation map_mx_sub := (fun f => @map_mx_sub _ _ f) (only parsing). diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v index 7e213b8..e65bc3c 100644 --- a/mathcomp/algebra/mxalgebra.v +++ b/mathcomp/algebra/mxalgebra.v @@ -2581,8 +2581,8 @@ rewrite mulmx_suml linear_sum summx_sub //= => i _. by rewrite -mulmxA !mem_mulsmx. Qed. -Lemma mulsmx_addl m1 m2 m3 n - (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) (R3 : 'A_(m3, n)) : +Lemma mulsmxDl m1 m2 m3 n + (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) (R3 : 'A_(m3, n)) : ((R1 + R2) * R3 = R1 * R3 + R2 * R3)%MS. Proof. rewrite -(genmx_muls R2 R3) -(genmx_muls R1 R3) -genmx_muls -genmx_adds. @@ -2591,8 +2591,8 @@ apply/mulsmx_subP=> _ A3 /memmx_addsP[A [R_A1 R_A2 ->]] R_A3. by rewrite mulmxDl linearD addmx_sub_adds ?mem_mulsmx. Qed. -Lemma mulsmx_addr m1 m2 m3 n - (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) (R3 : 'A_(m3, n)) : +Lemma mulsmxDr m1 m2 m3 n + (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) (R3 : 'A_(m3, n)) : (R1 * (R2 + R3) = R1 * R2 + R1 * R3)%MS. Proof. rewrite -(genmx_muls R1 R3) -(genmx_muls R1 R2) -genmx_muls -genmx_adds. @@ -2857,7 +2857,7 @@ set pAnz := [pred k | A k.1 k.2 != 0]. rewrite (@eq_pick _ _ pAnz) => [|k]; last by rewrite /= mxE fmorph_eq0. case: {+}(pick _) => [[i j]|]; last by rewrite !map_mx1. rewrite mxE -fmorphV -map_xcol -map_xrow -map_dlsubmx -map_drsubmx. -rewrite -map_ursubmx -map_mxZ -map_mxM -map_mx_sub {}IHm /=. +rewrite -map_ursubmx -map_mxZ -map_mxM -map_mxB {}IHm /=. case: {+}(Gaussian_elimination _) => [[L U] r] /=; rewrite map_xrow map_xcol. by rewrite !(@map_block_mx _ _ f 1 _ 1) !map_mx0 ?map_mx1 ?map_scalar_mx. Qed. @@ -2952,7 +2952,7 @@ by rewrite -!map_capmx !map_submx -!diffmxE andbb. Qed. Lemma map_eigenspace n (g : 'M_n) a : (eigenspace g a)^f = eigenspace g^f (f a). -Proof. by rewrite map_kermx map_mx_sub ?map_scalar_mx. Qed. +Proof. by rewrite map_kermx map_mxB ?map_scalar_mx. Qed. Lemma eigenvalue_map n (g : 'M_n) a : eigenvalue g^f (f a) = eigenvalue g a. Proof. by rewrite /eigenvalue -map_eigenspace map_mx_eq0. Qed. @@ -2972,12 +2972,18 @@ Qed. Lemma map_cent_mx m n (E : 'A_(m, n)) : ('C(E)%MS)^f = 'C(E^f)%MS. Proof. -rewrite map_kermx //; congr (kermx _); apply: map_lin_mx => // A. -rewrite map_mxM //; congr (_ *m _); apply: map_lin_mx => //= B. -by rewrite map_mx_sub ? map_mxM. +rewrite map_kermx; congr kermx; apply: map_lin_mx => A; rewrite map_mxM. +by congr (_ *m _); apply: map_lin_mx => B; rewrite map_mxB ?map_mxM. Qed. Lemma map_center_mx m n (E : 'A_(m, n)) : (('Z(E))^f :=: 'Z(E^f))%MS. Proof. by rewrite /center_mx -map_cent_mx; apply: map_capmx. Qed. End MapMatrixSpaces. + +Notation "@ 'mulsmx_addl'" := + (deprecate mulsmx_addl mulsmxDl) (at level 10, only parsing) : fun_scope. +Notation "@ 'mulsmx_addr'" := + (deprecate mulsmx_addr mulsmxDr) (at level 10, only parsing) : fun_scope. +Notation mulsmx_addl := (@mulsmx_addl _ _ _ _ _) (only parsing). +Notation mulsmx_addr := (@mulsmx_addr _ _ _ _ _) (only parsing). diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v index 74d524e..c7f8fb1 100644 --- a/mathcomp/algebra/mxpoly.v +++ b/mathcomp/algebra/mxpoly.v @@ -890,7 +890,7 @@ rewrite !big_cons; case: ifP => [Pj|PNj]; rewrite ?ihjs ?submx_refl//. suff cjjs: coprimep (p_ j) (\prod_(i <- js | P i) p_ i). by rewrite !kermxpolyM// !(adds_eqmx (eqmx_refl _) (ihjs _)) ?submx_refl. rewrite (@big_morph _ _ _ true andb) ?big_all_cond ?coprimep1//; last first. - by move=> p q; rewrite coprimep_mulr. + by move=> p q; rewrite coprimepMr. apply/allP => i i_js; apply/implyP => Pi; apply: p_coprime => //. by apply: contraNneq jNjs => <-. Qed. @@ -907,7 +907,7 @@ have cpNi : {in [pred j | P j && (j != i)] &, rewrite -!(cap_eqmx (eqmx_refl _) (kermxpoly_prod g _))//. rewrite mxdirect_kermxpoly ?submx_refl//. rewrite (@big_morph _ _ _ true andb) ?big_all_cond ?coprimep1//; last first. - by move=> p q; rewrite coprimep_mulr. + by move=> p q; rewrite coprimepMr. by apply/allP => j _; apply/implyP => /andP[Pj neq_ji]; apply: p_coprime. Qed. diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v index a33788d..e9e9c45 100644 --- a/mathcomp/algebra/poly.v +++ b/mathcomp/algebra/poly.v @@ -428,26 +428,25 @@ Lemma coef_sum I (r : seq I) (P : pred I) (F : I -> {poly R}) k : (\sum_(i <- r | P i) F i)`_k = \sum_(i <- r | P i) (F i)`_k. Proof. exact: (raddf_sum (coefp_additive k)). Qed. -Lemma polyC_add : {morph polyC : a b / a + b}. +Lemma polyCD : {morph polyC : a b / a + b}. Proof. by move=> a b; apply/polyP=> [[|i]]; rewrite coefD !coefC ?addr0. Qed. -Lemma polyC_opp : {morph polyC : c / - c}. +Lemma polyCN : {morph polyC : c / - c}. Proof. by move=> c; apply/polyP=> [[|i]]; rewrite coefN !coefC ?oppr0. Qed. -Lemma polyC_sub : {morph polyC : a b / a - b}. -Proof. by move=> a b; rewrite polyC_add polyC_opp. Qed. +Lemma polyCB : {morph polyC : a b / a - b}. +Proof. by move=> a b; rewrite polyCD polyCN. Qed. -Canonical polyC_additive := Additive polyC_sub. +Canonical polyC_additive := Additive polyCB. -Lemma polyC_muln n : {morph polyC : c / c *+ n}. -Proof. exact: raddfMn. Qed. +Lemma polyCMn n : {morph polyC : c / c *+ n}. Proof. exact: raddfMn. Qed. Lemma size_opp p : size (- p) = size p. Proof. by apply/eqP; rewrite eqn_leq -{3}(opprK p) -[-%R]/opp_poly unlock !size_poly. Qed. -Lemma lead_coef_opp p : lead_coef (- p) = - lead_coef p. +Lemma lead_coefN p : lead_coef (- p) = - lead_coef p. Proof. by rewrite /lead_coef size_opp coefN. Qed. Lemma size_add p q : size (p + q) <= maxn (size p) (size q). @@ -621,15 +620,14 @@ rewrite coefMr big_ord_recl subn0. by rewrite big1 => [|j _]; rewrite coefC !simp. Qed. -Lemma polyC_mul : {morph polyC : a b / a * b}. +Lemma polyCM : {morph polyC : a b / a * b}. Proof. by move=> a b; apply/polyP=> [[|i]]; rewrite coefCM !coefC ?simp. Qed. Fact polyC_multiplicative : multiplicative polyC. -Proof. by split; first apply: polyC_mul. Qed. +Proof. by split; first apply: polyCM. Qed. Canonical polyC_rmorphism := AddRMorphism polyC_multiplicative. -Lemma polyC_exp n : {morph polyC : c / c ^+ n}. -Proof. exact: rmorphX. Qed. +Lemma polyC_exp n : {morph polyC : c / c ^+ n}. Proof. exact: rmorphX. Qed. Lemma size_exp_leq p n : size (p ^+ n) <= ((size p).-1 * n).+1. Proof. @@ -665,7 +663,7 @@ by case: leqP => // le_p_n; rewrite nth_default ?mulr0. Qed. Fact scale_polyA a b p : scale_poly a (scale_poly b p) = scale_poly (a * b) p. -Proof. by rewrite !scale_polyE mulrA polyC_mul. Qed. +Proof. by rewrite !scale_polyE mulrA polyCM. Qed. Fact scale_1poly : left_id 1 scale_poly. Proof. by move=> p; rewrite scale_polyE mul1r. Qed. @@ -761,9 +759,7 @@ by elim: {p}(p : seq R) => //= p c IHp; rewrite cons_poly_def; apply: Kcons. Qed. Lemma polyseqXsubC a : 'X - a%:P = [:: - a; 1] :> seq R. -Proof. -by rewrite -['X]mul1r -polyC_opp -cons_poly_def polyseq_cons polyseq1. -Qed. +Proof. by rewrite -['X]mul1r -polyCN -cons_poly_def polyseq_cons polyseq1. Qed. Lemma size_XsubC a : size ('X - a%:P) = 2%N. Proof. by rewrite polyseqXsubC. Qed. @@ -843,7 +839,7 @@ Lemma poly_def n E : \poly_(i < n) E i = \sum_(i < n) E i *: 'X^i. Proof. rewrite unlock; elim: n => [|n IHn] in E *; first by rewrite big_ord0. rewrite big_ord_recl /= cons_poly_def addrC expr0 alg_polyC. -congr (_ + _); rewrite (iota_addl 1 0) -map_comp IHn big_distrl /=. +congr (_ + _); rewrite (iotaDl 1 0) -map_comp IHn big_distrl /=. by apply: eq_bigr => i _; rewrite -scalerAl exprSr. Qed. @@ -1065,7 +1061,7 @@ Proof. by elim/big_rec2: _ => [|i _ p _ <-]; rewrite (horner0, hornerD). Qed. Lemma hornerCM a p x : (a%:P * p).[x] = a * p.[x]. Proof. elim/poly_ind: p => [|p c IHp]; first by rewrite !(mulr0, horner0). -by rewrite mulrDr mulrA -polyC_mul !hornerMXaddC IHp mulrDr mulrA. +by rewrite mulrDr mulrA -polyCM !hornerMXaddC IHp mulrDr mulrA. Qed. Lemma hornerZ c p x : (c *: p).[x] = c * p.[x]. @@ -1528,7 +1524,7 @@ Proof. by case: n => // n; rewrite derivSn derivC linear0. Qed. Lemma derivnD n : {morph derivn n : p q / p + q}. Proof. exact: linearD. Qed. -Lemma derivn_sub n : {morph derivn n : p q / p - q}. +Lemma derivnB n : {morph derivn n : p q / p - q}. Proof. exact: linearB. Qed. Lemma derivnMn n m p : (p *+ m)^`(n) = p^`(n) *+ m. @@ -2219,7 +2215,7 @@ Definition poly_inv p := if p \in poly_unit then (p`_0)^-1%:P else p. Fact poly_mulVp : {in poly_unit, left_inverse 1 poly_inv *%R}. Proof. move=> p Up; rewrite /poly_inv Up. -by case/andP: Up => /size_poly1P[c _ ->]; rewrite coefC -polyC_mul => /mulVr->. +by case/andP: Up => /size_poly1P[c _ ->]; rewrite coefC -polyCM => /mulVr->. Qed. Fact poly_intro_unit p q : q * p = 1 -> p \in poly_unit. @@ -2264,7 +2260,7 @@ Proof. by []. Qed. Lemma poly_invE p : p ^-1 = if p \in GRing.unit then (p`_0)^-1%:P else p. Proof. by []. Qed. -Lemma polyC_inv c : c%:P^-1 = (c^-1)%:P. +Lemma polyCV c : c%:P^-1 = (c^-1)%:P. Proof. have [/rmorphV-> // | nUc] := boolP (c \in GRing.unit). by rewrite !invr_out // poly_unitE coefC (negbTE nUc) andbF. @@ -2771,3 +2767,28 @@ by rewrite monic_prod => // i; rewrite monicXsubC. Qed. End ClosedField. + +Notation "@ 'polyC_add'" := + (deprecate polyC_add polyCD) (at level 10, only parsing) : fun_scope. +Notation "@ 'polyC_opp'" := + (deprecate polyC_opp polyCN) (at level 10, only parsing) : fun_scope. +Notation "@ 'polyC_sub'" := + (deprecate polyC_sub polyCB) (at level 10, only parsing) : fun_scope. +Notation "@ 'polyC_muln'" := + (deprecate polyC_muln polyCMn) (at level 10, only parsing) : fun_scope. +Notation "@ 'polyC_mul'" := + (deprecate polyC_mul polyCM) (at level 10, only parsing) : fun_scope. +Notation "@ 'polyC_inv'" := + (deprecate polyC_inv polyCV) (at level 10, only parsing) : fun_scope. +Notation "@ 'lead_coef_opp'" := + (deprecate lead_coef_opp lead_coefN) (at level 10, only parsing) : fun_scope. +Notation "@ 'derivn_sub'" := + (deprecate derivn_sub derivnB) (at level 10, only parsing) : fun_scope. +Notation polyC_add := (@polyC_add _) (only parsing). +Notation polyC_opp := (@polyC_opp _) (only parsing). +Notation polyC_sub := (@polyC_sub _) (only parsing). +Notation polyC_muln := (@polyC_muln _) (only parsing). +Notation polyC_mul := (@polyC_mul _) (only parsing). +Notation polyC_inv := (@polyC_inv _) (only parsing). +Notation lead_coef_opp := (@lead_coef_opp _) (only parsing). +Notation derivn_sub := (@derivn_sub _) (only parsing). diff --git a/mathcomp/algebra/polyXY.v b/mathcomp/algebra/polyXY.v index 9bc8fd5..fe0acb4 100644 --- a/mathcomp/algebra/polyXY.v +++ b/mathcomp/algebra/polyXY.v @@ -228,7 +228,7 @@ Proof. by rewrite -!size_poly_eq0 size_poly_XmY. Qed. Lemma lead_coef_poly_XaY p : lead_coef (poly_XaY p) = (lead_coef p)%:P. Proof. -rewrite lead_coef_comp ?size_XaddC // -['Y]opprK -polyC_opp lead_coefXsubC. +rewrite lead_coef_comp ?size_XaddC // -['Y]opprK -polyCN lead_coefXsubC. by rewrite expr1n mulr1 lead_coef_map_inj //; apply: polyC_inj. Qed. diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v index a7d3b1e..8459c45 100644 --- a/mathcomp/algebra/polydiv.v +++ b/mathcomp/algebra/polydiv.v @@ -365,7 +365,7 @@ elim: (size m) 0%N 0 {1 4 6}m (leqnn (size m)) => [|n IHn] k q r Hr /=. by rewrite size_poly0 size_poly_gt0. case: ltnP => Hlt Heq; first by constructor. apply/IHn=> [|Cda]; last first. - rewrite mulrDl addrAC -addrA subrK exprSr polyC_mul mulrA Heq //. + rewrite mulrDl addrAC -addrA subrK exprSr polyCM mulrA Heq //. by rewrite mulrDl -mulrA Cda mulrA. apply/leq_sizeP => j Hj; rewrite coefB coefMC -scalerAl coefZ coefXnM. rewrite ltn_subRL ltnNge (leq_trans Hr) /=; last first. @@ -465,7 +465,7 @@ suff: by rewrite rreg_size ?ltn_rmodp //; exact: rregX. rewrite mulrDl addrAC mulNr -!mulrA polyC_exp -(commrX (m-v) Cdl). rewrite -polyC_exp mulrA -mulrDl -rdivp_eq // [(_ ^+ (m - k))%:P]polyC_exp. -rewrite -(commrX (m-k) Cdl) -polyC_exp mulrA -he -!mulrA -!polyC_mul -/v. +rewrite -(commrX (m-k) Cdl) -polyC_exp mulrA -he -!mulrA -!polyCM -/v. by rewrite -!exprD addnC subnK ?leq_maxl // addnC subnK ?subrr ?leq_maxr. Qed. @@ -553,15 +553,15 @@ case: (monic_comreg mond)=> Hc Hr; rewrite [r in _ * _ + r]rdivp_eq addrA. by rewrite -mulrDl rdivp_addl_mul_small // ltn_rmodp monic_neq0. Qed. -Lemma rdivp_addl q r : rdvdp d q -> rdivp (q + r) d = rdivp q d + rdivp r d. +Lemma rdivpDl q r : rdvdp d q -> rdivp (q + r) d = rdivp q d + rdivp r d. Proof. case: (monic_comreg mond)=> Hc Hr; rewrite [r in q + r]rdivp_eq addrA. rewrite [q in q + _ + _]rdivp_eq; move/rmodp_eq0P->. by rewrite addr0 -mulrDl rdivp_addl_mul_small // ltn_rmodp monic_neq0. Qed. -Lemma rdivp_addr q r : rdvdp d r -> rdivp (q + r) d = rdivp q d + rdivp r d. -Proof. by rewrite addrC; move/rdivp_addl->; rewrite addrC. Qed. +Lemma rdivpDr q r : rdvdp d r -> rdivp (q + r) d = rdivp q d + rdivp r d. +Proof. by rewrite addrC; move/rdivpDl->; rewrite addrC. Qed. Lemma rdivp_mull p : rdivp (p * d) d = p. Proof. by rewrite -[p * d]addr0 rdivp_addl_mul rdiv0p addr0. Qed. @@ -581,7 +581,7 @@ Proof. by move=> Hd; case: (monic_comreg mond)=> Hc Hr; rewrite /rmodp redivp_eq. Qed. -Lemma rmodp_add p q : rmodp (p + q) d = rmodp p d + rmodp q d. +Lemma rmodpD p q : rmodp (p + q) d = rmodp p d + rmodp q d. Proof. rewrite [p in LHS]rdivp_eq [q in LHS]rdivp_eq addrACA -mulrDl. rewrite rmodp_addl_mul_small //; apply: (leq_ltn_trans (size_add _ _)). @@ -590,7 +590,7 @@ Qed. Lemma rmodp_mulmr p q : rmodp (p * (rmodp q d)) d = rmodp (p * q) d. Proof. -by rewrite [q in RHS]rdivp_eq mulrDr rmodp_add mulrA rmodp_mull add0r. +by rewrite [q in RHS]rdivp_eq mulrDr rmodpD mulrA rmodp_mull add0r. Qed. Lemma rdvdpp : rdvdp d d. @@ -623,6 +623,19 @@ Lemma rdivpK p : rdvdp d p -> (rdivp p d) * d = p. Proof. by move=> dvddp; rewrite [RHS]rdivp_eq rmodp_eq0 ?addr0. Qed. End MonicDivisor. + +Notation "@ 'rdivp_addl'" := + (deprecate rdivp_addl rdivpDl) (at level 10, only parsing) : fun_scope. +Notation "@ 'rdivp_addr'" := + (deprecate rdivp_addr rdivpDr) (at level 10, only parsing) : fun_scope. +Notation "@ 'rmodp_add'" := + (deprecate rmodp_add rmodpD) (at level 10, only parsing) : fun_scope. +Notation rdivp_addl := + (fun d_monic => @rdivp_addl _ _ d_monic _) (only parsing). +Notation rdivp_addr := + (fun d_monic q => @rdivp_addr _ _ d_monic q _) (only parsing). +Notation rmodp_add := (@rmodp_add _ _) (only parsing). + End RingMonic. Module Ring. @@ -824,7 +837,7 @@ rewrite unlock ud redivp_def; constructor => //. rewrite -scalerAl -scalerDr -mul_polyC. have hn0 : (lead_coef d ^+ rscalp m d)%:P != 0. by rewrite polyC_eq0; apply: expf_neq0. - apply: (mulfI hn0); rewrite !mulrA -exprVn !polyC_exp -exprMn -polyC_mul. + apply: (mulfI hn0); rewrite !mulrA -exprVn !polyC_exp -exprMn -polyCM. by rewrite divrr // expr1n mul1r -polyC_exp mul_polyC rdivp_eq. move=> dn0; rewrite size_scale ?ltn_rmodp // -exprVn expf_eq0 negb_and. by rewrite invr_eq0 cdn0 orbT. @@ -1415,13 +1428,18 @@ suff Hmn m n: m %= n -> (m %| p) -> (n %| p). by rewrite /eqp; case/andP=> dd' d'd dp; apply: (dvdp_trans d'd). Qed. -Lemma dvdp_scaler c m n : c != 0 -> m %| c *: n = (m %| n). +Lemma dvdpZr c m n : c != 0 -> m %| c *: n = (m %| n). Proof. by move=> cn0; exact/eqp_dvdr/eqp_scale. Qed. -Lemma dvdp_scalel c m n : c != 0 -> (c *: m %| n) = (m %| n). +Lemma dvdpZl c m n : c != 0 -> (c *: m %| n) = (m %| n). Proof. by move=> cn0; exact/eqp_dvdl/eqp_scale. Qed. -Lemma dvdp_opp d p : d %| (- p) = (d %| p). +Lemma dvdpNl d p : (- d) %| p = (d %| p). +Proof. +by rewrite -scaleN1r; apply/eqp_dvdl/eqp_scale; rewrite oppr_eq0 oner_neq0. +Qed. + +Lemma dvdpNr d p : d %| (- p) = (d %| p). Proof. by apply: eqp_dvdr; rewrite -scaleN1r eqp_scale ?oppr_eq0 ?oner_eq0. Qed. Lemma eqp_mul2r r p q : r != 0 -> (p * r %= q * r) = (p %= q). @@ -1660,7 +1678,7 @@ rewrite (polySpred mn0) addSn /= -[n in _ <= n]add0n leq_add2r -ltnS. rewrite -polySpred //= leq_eqVlt ltnS size_poly_leq0 (negPf mn0) orbF. case/size_poly1P=> c cn0 -> {mn0 m}; rewrite mul_polyC. suff -> : n %% (c *: n) = 0 by rewrite gcd0p; apply: eqp_scale. -by apply/modp_eq0P; rewrite dvdp_scalel. +by apply/modp_eq0P; rewrite dvdpZl. Qed. Lemma gcdp_mulr m n : gcdp n (n * m) %= n. @@ -1670,8 +1688,8 @@ Lemma gcdp_scalel c m n : c != 0 -> gcdp (c *: m) n %= gcdp m n. Proof. move=> cn0; rewrite /eqp dvdp_gcd [gcdp m n %| _]dvdp_gcd !dvdp_gcdr !andbT. apply/andP; split; last first. - by apply: dvdp_trans (dvdp_gcdl _ _) _; rewrite dvdp_scaler. -by apply: dvdp_trans (dvdp_gcdl _ _) _; rewrite dvdp_scalel. + by apply: dvdp_trans (dvdp_gcdl _ _) _; rewrite dvdpZr. +by apply: dvdp_trans (dvdp_gcdl _ _) _; rewrite dvdpZl. Qed. Lemma gcdp_scaler c m n : c != 0 -> gcdp m (c *: n) %= gcdp m n. @@ -1764,10 +1782,10 @@ Proof. by rewrite /coprimep=> /eqP. Qed. Lemma coprimep_def p q : coprimep p q = (size (gcdp p q) == 1%N). Proof. done. Qed. -Lemma coprimep_scalel c m n : c != 0 -> coprimep (c *: m) n = coprimep m n. +Lemma coprimepZl c m n : c != 0 -> coprimep (c *: m) n = coprimep m n. Proof. by move=> ?; rewrite !coprimep_def (eqp_size (gcdp_scalel _ _ _)). Qed. -Lemma coprimep_scaler c m n: c != 0 -> coprimep m (c *: n) = coprimep m n. +Lemma coprimepZr c m n: c != 0 -> coprimep m (c *: n) = coprimep m n. Proof. by move=> ?; rewrite !coprimep_def (eqp_size (gcdp_scaler _ _ _)). Qed. Lemma coprimepp p : coprimep p p = (size p == 1%N). @@ -1981,7 +1999,7 @@ Qed. Lemma Gauss_gcdpl p m n : coprimep p n -> gcdp p (m * n) %= gcdp p m. Proof. by move=> co_pn; rewrite mulrC Gauss_gcdpr. Qed. -Lemma coprimep_mulr p q r : coprimep p (q * r) = (coprimep p q && coprimep p r). +Lemma coprimepMr p q r : coprimep p (q * r) = (coprimep p q && coprimep p r). Proof. apply/coprimepP/andP=> [hp | [/coprimepP-hq hr]]. by split; apply/coprimepP=> d dp dq; rewrite hp //; @@ -1991,8 +2009,8 @@ rewrite Gauss_dvdpl in dqr; first exact: hq. by move/coprimep_dvdr: hr; apply. Qed. -Lemma coprimep_mull p q r: coprimep (q * r) p = (coprimep q p && coprimep r p). -Proof. by rewrite ![coprimep _ p]coprimep_sym coprimep_mulr. Qed. +Lemma coprimepMl p q r: coprimep (q * r) p = (coprimep q p && coprimep r p). +Proof. by rewrite ![coprimep _ p]coprimep_sym coprimepMr. Qed. Lemma modp_coprime k u n : k != 0 -> (k * u) %% n %= 1 -> coprimep k n. Proof. @@ -2005,7 +2023,7 @@ Qed. Lemma coprimep_pexpl k m n : 0 < k -> coprimep (m ^+ k) n = coprimep m n. Proof. case: k => // k _; elim: k => [|k IHk]; first by rewrite expr1. -by rewrite exprS coprimep_mull -IHk andbb. +by rewrite exprS coprimepMl -IHk andbb. Qed. Lemma coprimep_pexpr k m n : 0 < k -> coprimep m (n ^+ k) = coprimep m n. @@ -2108,8 +2126,8 @@ have dn0 : d != 0 by rewrite gcdp_eq0 negb_and nn0 orbT. have c1n0 : c1 != 0 by rewrite !expf_neq0 // lead_coef_eq0. have c2n0 : c2 != 0 by rewrite !expf_neq0 // lead_coef_eq0. have c2k_n0 : c2 ^+ k != 0 by rewrite !expf_neq0 // lead_coef_eq0. -rewrite -(@dvdp_scaler (c1 ^+ k)) ?expf_neq0 ?lead_coef_eq0 //. -rewrite -(@dvdp_scalel (c2 ^+ k)) // -!exprZn def_m def_n !exprMn. +rewrite -(@dvdpZr (c1 ^+ k)) ?expf_neq0 ?lead_coef_eq0 //. +rewrite -(@dvdpZl (c2 ^+ k)) // -!exprZn def_m def_n !exprMn. rewrite dvdp_mul2r ?expf_neq0 //. have: coprimep (m' ^+ k) (n' ^+ k). by rewrite coprimep_pexpl // coprimep_pexpr // coprimep_div_gcd ?mn0. @@ -2120,8 +2138,8 @@ have /size_poly1P [c cn0 em'] : size m' == 1%N. have := hc _ (dvdpp _) hd; rewrite -size_poly_eq1. rewrite polySpred; last by rewrite expf_eq0 negb_and m'_n0 orbT. by rewrite size_exp eqSS muln_eq0 orbC eqn0Ngt k_gt0 /= -eqSS -polySpred. -rewrite -(@dvdp_scalel c2) // def_m em' mul_polyC dvdp_scalel //. -by rewrite -(@dvdp_scaler c1) // def_n dvdp_mull. +rewrite -(@dvdpZl c2) // def_m em' mul_polyC dvdpZl //. +by rewrite -(@dvdpZr c1) // def_n dvdp_mull. Qed. Lemma root_gcd p q x : root (gcdp p q) x = root p x && root q x. @@ -2285,7 +2303,7 @@ Qed. Lemma coprimep_XsubC p c : coprimep p ('X - c%:P) = ~~ root p c. Proof. rewrite -coprimep_modl modp_XsubC /root -alg_polyC. -have [-> | /coprimep_scalel->] := eqVneq; last exact: coprime1p. +have [-> | /coprimepZl->] := eqVneq; last exact: coprime1p. by rewrite scale0r /coprimep gcd0p size_XsubC. Qed. @@ -2340,6 +2358,28 @@ End IDomainPseudoDivision. Hint Resolve eqpxx divp0 divp1 mod0p modp0 modp1 dvdp_mull dvdp_mulr dvdpp : core. Hint Resolve dvdp0 : core. +Notation "@ 'dvdp_scalel'" := + (deprecate dvdp_scalel dvdpZl) (at level 10, only parsing) : fun_scope. +Notation "@ 'dvdp_scaler'" := + (deprecate dvdp_scaler dvdpZr) (at level 10, only parsing) : fun_scope. +Notation "@ 'dvdp_opp'" := + (deprecate dvdp_opp dvdpNr) (at level 10, only parsing) : fun_scope. +Notation "@ 'coprimep_scalel'" := + (deprecate coprimep_scalel coprimepZl) (at level 10, only parsing) : fun_scope. +Notation "@ 'coprimep_scaler'" := + (deprecate coprimep_scaler coprimepZr) (at level 10, only parsing) : fun_scope. +Notation "@ 'coprimep_mull'" := + (deprecate coprimep_mull coprimepMl) (at level 10, only parsing) : fun_scope. +Notation "@ 'coprimep_mulr'" := + (deprecate coprimep_mulr coprimepMr) (at level 10, only parsing) : fun_scope. +Notation dvdp_scalel := (@dvdp_scalel _ _) (only parsing). +Notation dvdp_scaler := (@dvdp_scaler _ _) (only parsing). +Notation dvdp_opp := (@dvdp_opp _) (only parsing). +Notation coprimep_scalel := (@coprimep_scalel _ _) (only parsing). +Notation coprimep_scaler := (@coprimep_scaler _ _) (only parsing). +Notation coprimep_mull := (@coprimep_mull _) (only parsing). +Notation coprimep_mulr := (@coprimep_mulr _) (only parsing). + End CommonIdomain. Module Idomain. @@ -2461,7 +2501,7 @@ move=> ulcq /eqp_eq; move/(congr1 ( *:%R (lead_coef q)^-1 )). by rewrite !scalerA mulrC divrr // scale1r mulrC. Qed. -Lemma modp_scalel c p : (c *: p) %% d = c *: (p %% d). +Lemma modpZl c p : (c *: p) %% d = c *: (p %% d). Proof. have [-> | cn0] := eqVneq c 0; first by rewrite !scale0r mod0p. have e : (c *: p) = (c *: (p %/ d)) * d + c *: (p %% d). @@ -2472,7 +2512,7 @@ rewrite size_polyC cn0 addSn add0n /= ltn_modp -lead_coef_eq0. by apply: contraTneq ulcd => ->; rewrite unitr0. Qed. -Lemma divp_scalel c p : (c *: p) %/ d = c *: (p %/ d). +Lemma divpZl c p : (c *: p) %/ d = c *: (p %/ d). Proof. have [-> | cn0] := eqVneq c 0; first by rewrite !scale0r div0p. have e : (c *: p) = (c *: (p %/ d)) * d + c *: (p %% d). @@ -2486,22 +2526,22 @@ Qed. Lemma eqp_modpl p q : p %= q -> (p %% d) %= (q %% d). Proof. case/eqpP=> [[c1 c2]] /andP /= [c1n0 c2n0 e]. -by apply/eqpP; exists (c1, c2); rewrite ?c1n0 //= -!modp_scalel e. +by apply/eqpP; exists (c1, c2); rewrite ?c1n0 //= -!modpZl e. Qed. Lemma eqp_divl p q : p %= q -> (p %/ d) %= (q %/ d). Proof. case/eqpP=> [[c1 c2]] /andP /= [c1n0 c2n0 e]. -by apply/eqpP; exists (c1, c2); rewrite ?c1n0 // -!divp_scalel e. +by apply/eqpP; exists (c1, c2); rewrite ?c1n0 // -!divpZl e. Qed. -Lemma modp_opp p : (- p) %% d = - (p %% d). -Proof. by rewrite -mulN1r -[RHS]mulN1r -polyC_opp !mul_polyC modp_scalel. Qed. +Lemma modpN p : (- p) %% d = - (p %% d). +Proof. by rewrite -mulN1r -[RHS]mulN1r -polyCN !mul_polyC modpZl. Qed. -Lemma divp_opp p : (- p) %/ d = - (p %/ d). -Proof. by rewrite -mulN1r -[RHS]mulN1r -polyC_opp !mul_polyC divp_scalel. Qed. +Lemma divpN p : (- p) %/ d = - (p %/ d). +Proof. by rewrite -mulN1r -[RHS]mulN1r -polyCN !mul_polyC divpZl. Qed. -Lemma modp_add p q : (p + q) %% d = p %% d + q %% d. +Lemma modpD p q : (p + q) %% d = p %% d + q %% d. Proof. have/edivpP [] // : (p + q) = (p %/ d + q %/ d) * d + (p %% d + q %% d). by rewrite mulrDl addrACA -!divp_eq. @@ -2510,7 +2550,7 @@ rewrite gtn_max !ltn_modp andbb -lead_coef_eq0. by apply: contraTneq ulcd => ->; rewrite unitr0. Qed. -Lemma divp_add p q : (p + q) %/ d = p %/ d + q %/ d. +Lemma divpD p q : (p + q) %/ d = p %/ d + q %/ d. Proof. have/edivpP [] // : (p + q) = (p %/ d + q %/ d) * d + (p %% d + q %% d). by rewrite mulrDl addrACA -!divp_eq. @@ -2527,16 +2567,14 @@ Qed. Lemma mulKp q : (d * q) %/ d = q. Proof. by rewrite mulrC; apply: mulpK. Qed. -Lemma divp_addl_mul_small q r : - size r < size d -> (q * d + r) %/ d = q. -Proof. by move=> srd; rewrite divp_add (divp_small srd) addr0 mulpK. Qed. +Lemma divp_addl_mul_small q r : size r < size d -> (q * d + r) %/ d = q. +Proof. by move=> srd; rewrite divpD (divp_small srd) addr0 mulpK. Qed. -Lemma modp_addl_mul_small q r : - size r < size d -> (q * d + r) %% d = r. -Proof. by move=> srd; rewrite modp_add modp_mull add0r modp_small. Qed. +Lemma modp_addl_mul_small q r : size r < size d -> (q * d + r) %% d = r. +Proof. by move=> srd; rewrite modpD modp_mull add0r modp_small. Qed. Lemma divp_addl_mul q r : (q * d + r) %/ d = q + r %/ d. -Proof. by rewrite divp_add mulpK. Qed. +Proof. by rewrite divpD mulpK. Qed. Lemma divpp : d %/ d = 1. Proof. by rewrite -[d in d %/ _]mul1r mulpK. Qed. @@ -2584,7 +2622,7 @@ Lemma divp_mulCA p q : d %| p -> d %| q -> p * (q %/ d) = q * (p %/ d). Proof. by move=> hdp hdq; rewrite mulrC divp_mulAC // divp_mulA. Qed. Lemma modp_mul p q : (p * (q %% d)) %% d = (p * q) %% d. -Proof. by rewrite [q in RHS]divp_eq mulrDr modp_add mulrA modp_mull add0r. Qed. +Proof. by rewrite [q in RHS]divp_eq mulrDr modpD mulrA modp_mull add0r. Qed. End UnitDivisor. @@ -2644,7 +2682,7 @@ Qed. Lemma divpAC p q : lead_coef p \in GRing.unit -> q %/ d %/ p = q %/ p %/ d. Proof. by move=> ulcp; rewrite !divp_divl // mulrC. Qed. -Lemma modp_scaler c p : c \in GRing.unit -> p %% (c *: d) = (p %% d). +Lemma modpZr c p : c \in GRing.unit -> p %% (c *: d) = (p %% d). Proof. case: (eqVneq d 0) => [-> | dn0 cn0]; first by rewrite scaler0 !modp0. have e : p = (c^-1 *: (p %/ d)) * (c *: d) + (p %% d). @@ -2654,7 +2692,7 @@ suff s : size (p %% d) < size (c *: d). by rewrite size_scale ?ltn_modp //; apply: contraTneq cn0 => ->; rewrite unitr0. Qed. -Lemma divp_scaler c p : c \in GRing.unit -> p %/ (c *: d) = c^-1 *: (p %/ d). +Lemma divpZr c p : c \in GRing.unit -> p %/ (c *: d) = c^-1 *: (p %/ d). Proof. case: (eqVneq d 0) => [-> | dn0 cn0]; first by rewrite scaler0 !divp0 scaler0. have e : p = (c^-1 *: (p %/ d)) * (c *: d) + (p %% d). @@ -2666,6 +2704,31 @@ Qed. End MoreUnitDivisor. +Notation "@ 'modp_scalel'" := + (deprecate modp_scalel modpZl) (at level 10, only parsing) : fun_scope. +Notation "@ 'modp_scaler'" := + (deprecate modp_scaler modpZr) (at level 10, only parsing) : fun_scope. +Notation "@ 'modp_opp'" := + (deprecate modp_opp modpN) (at level 10, only parsing) : fun_scope. +Notation "@ 'modp_add'" := + (deprecate modp_add modpD) (at level 10, only parsing) : fun_scope. +Notation "@ 'divp_scalel'" := + (deprecate divp_scalel divpZl) (at level 10, only parsing) : fun_scope. +Notation "@ 'divp_scaler'" := + (deprecate divp_scaler divpZr) (at level 10, only parsing) : fun_scope. +Notation "@ 'divp_opp'" := + (deprecate divp_opp divpN) (at level 10, only parsing) : fun_scope. +Notation "@ 'divp_add'" := + (deprecate divp_add divpD) (at level 10, only parsing) : fun_scope. +Notation modp_scalel := (@modp_scalel _ _) (only parsing). +Notation modp_scaler := (fun d_unit => @modp_scaler _ _ d_unit _) (only parsing). +Notation modp_opp := (@modp_opp _ _) (only parsing). +Notation modp_add := (@modp_add _ _) (only parsing). +Notation divp_scalel := (@divp_scalel _ _) (only parsing). +Notation divp_scaler := (fun d_unit => @divp_scaler _ _ d_unit _) (only parsing). +Notation divp_opp := (@divp_opp _ _) (only parsing). +Notation divp_add := (@divp_add _ _) (only parsing). + End IdomainUnit. Module Field. @@ -2724,10 +2787,10 @@ case/IdomainUnit.ulc_eqpP; first by rewrite unitfE lead_coef_eq0. by move=> c nz_c ->; exists c. Qed. -Lemma modp_scalel c p q : (c *: p) %% q = c *: (p %% q). +Lemma modpZl c p q : (c *: p) %% q = c *: (p %% q). Proof. have [-> | qn0] := eqVneq q 0; first by rewrite !modp0. -by apply: IdomainUnit.modp_scalel; rewrite unitfE lead_coef_eq0. +by apply: IdomainUnit.modpZl; rewrite unitfE lead_coef_eq0. Qed. Lemma mulpK p q : q != 0 -> p * q %/ q = p. @@ -2736,13 +2799,13 @@ Proof. by move=> qn0; rewrite IdomainUnit.mulpK // unitfE lead_coef_eq0. Qed. Lemma mulKp p q : q != 0 -> q * p %/ q = p. Proof. by rewrite mulrC; apply: mulpK. Qed. -Lemma divp_scalel c p q : (c *: p) %/ q = c *: (p %/ q). +Lemma divpZl c p q : (c *: p) %/ q = c *: (p %/ q). Proof. have [-> | qn0] := eqVneq q 0; first by rewrite !divp0 scaler0. -by apply: IdomainUnit.divp_scalel; rewrite unitfE lead_coef_eq0. +by apply: IdomainUnit.divpZl; rewrite unitfE lead_coef_eq0. Qed. -Lemma modp_scaler c p d : c != 0 -> p %% (c *: d) = (p %% d). +Lemma modpZr c p d : c != 0 -> p %% (c *: d) = (p %% d). Proof. case: (eqVneq d 0) => [-> | dn0 cn0]; first by rewrite scaler0 !modp0. have e : p = (c^-1 *: (p %/ d)) * (c *: d) + (p %% d). @@ -2751,7 +2814,7 @@ suff s : size (p %% d) < size (c *: d) by rewrite (modpP e s). by rewrite size_scale ?ltn_modp. Qed. -Lemma divp_scaler c p d : c != 0 -> p %/ (c *: d) = c^-1 *: (p %/ d). +Lemma divpZr c p d : c != 0 -> p %/ (c *: d) = c^-1 *: (p %/ d). Proof. case: (eqVneq d 0) => [-> | dn0 cn0]; first by rewrite scaler0 !divp0 scaler0. have e : p = (c^-1 *: (p %/ d)) * (c *: d) + (p %% d). @@ -2763,20 +2826,20 @@ Qed. Lemma eqp_modpl d p q : p %= q -> (p %% d) %= (q %% d). Proof. case/eqpP=> [[c1 c2]] /andP /= [c1n0 c2n0 e]. -by apply/eqpP; exists (c1, c2); rewrite ?c1n0 // -!modp_scalel e. +by apply/eqpP; exists (c1, c2); rewrite ?c1n0 // -!modpZl e. Qed. Lemma eqp_divl d p q : p %= q -> (p %/ d) %= (q %/ d). Proof. case/eqpP=> [[c1 c2]] /andP /= [c1n0 c2n0 e]. -by apply/eqpP; exists (c1, c2); rewrite ?c1n0 // -!divp_scalel e. +by apply/eqpP; exists (c1, c2); rewrite ?c1n0 // -!divpZl e. Qed. Lemma eqp_modpr d p q : p %= q -> (d %% p) %= (d %% q). Proof. case/eqpP=> [[c1 c2]] /andP [c1n0 c2n0 e]. have -> : p = (c1^-1 * c2) *: q by rewrite -scalerA -e scalerA mulVf // scale1r. -by rewrite modp_scaler ?eqpxx // mulf_eq0 negb_or invr_eq0 c1n0. +by rewrite modpZr ?eqpxx // mulf_eq0 negb_or invr_eq0 c1n0. Qed. Lemma eqp_mod p1 p2 q1 q2 : p1 %= p2 -> q1 %= q2 -> p1 %% q1 %= p2 %% q2. @@ -2786,7 +2849,7 @@ Lemma eqp_divr (d m n : {poly F}) : m %= n -> (d %/ m) %= (d %/ n). Proof. case/eqpP=> [[c1 c2]] /andP [c1n0 c2n0 e]. have -> : m = (c1^-1 * c2) *: n by rewrite -scalerA -e scalerA mulVf // scale1r. -by rewrite divp_scaler ?eqp_scale // ?invr_eq0 mulf_eq0 negb_or invr_eq0 c1n0. +by rewrite divpZr ?eqp_scale // ?invr_eq0 mulf_eq0 negb_or invr_eq0 c1n0. Qed. Lemma eqp_div p1 p2 q1 q2 : p1 %= p2 -> q1 %= q2 -> p1 %/ q1 %= p2 %/ q2. @@ -2823,37 +2886,37 @@ case: ifP=> // _; apply: ihn => //; apply: eqp_trans (eqp_rdiv_div _ _) _. by apply: eqp_div => //; apply: eqp_trans (eqp_rgcd_gcd _ _) _; apply: eqp_gcd. Qed. -Lemma modp_add d p q : (p + q) %% d = p %% d + q %% d. +Lemma modpD d p q : (p + q) %% d = p %% d + q %% d. Proof. have [-> | dn0] := eqVneq d 0; first by rewrite !modp0. -by apply: IdomainUnit.modp_add; rewrite unitfE lead_coef_eq0. +by apply: IdomainUnit.modpD; rewrite unitfE lead_coef_eq0. Qed. -Lemma modp_opp p q : (- p) %% q = - (p %% q). -Proof. by apply/eqP; rewrite -addr_eq0 -modp_add addNr mod0p. Qed. +Lemma modpN p q : (- p) %% q = - (p %% q). +Proof. by apply/eqP; rewrite -addr_eq0 -modpD addNr mod0p. Qed. -Lemma modNp p q : (- p) %% q = - (p %% q). Proof. exact: modp_opp. Qed. +Lemma modNp p q : (- p) %% q = - (p %% q). Proof. exact: modpN. Qed. -Lemma divp_add d p q : (p + q) %/ d = p %/ d + q %/ d. +Lemma divpD d p q : (p + q) %/ d = p %/ d + q %/ d. Proof. have [-> | dn0] := eqVneq d 0; first by rewrite !divp0 addr0. -by apply: IdomainUnit.divp_add; rewrite unitfE lead_coef_eq0. +by apply: IdomainUnit.divpD; rewrite unitfE lead_coef_eq0. Qed. -Lemma divp_opp p q : (- p) %/ q = - (p %/ q). -Proof. by apply/eqP; rewrite -addr_eq0 -divp_add addNr div0p. Qed. +Lemma divpN p q : (- p) %/ q = - (p %/ q). +Proof. by apply/eqP; rewrite -addr_eq0 -divpD addNr div0p. Qed. Lemma divp_addl_mul_small d q r : size r < size d -> (q * d + r) %/ d = q. Proof. -move=> srd; rewrite divp_add (divp_small srd) addr0 mulpK //. -by rewrite -size_poly_gt0; apply: leq_trans srd. +move=> srd; rewrite divpD (divp_small srd) addr0 mulpK // -size_poly_gt0. +exact: leq_trans srd. Qed. Lemma modp_addl_mul_small d q r : size r < size d -> (q * d + r) %% d = r. -Proof. by move=> srd; rewrite modp_add modp_mull add0r modp_small. Qed. +Proof. by move=> srd; rewrite modpD modp_mull add0r modp_small. Qed. Lemma divp_addl_mul d q r : d != 0 -> (q * d + r) %/ d = q + r %/ d. -Proof. by move=> dn0; rewrite divp_add mulpK. Qed. +Proof. by move=> dn0; rewrite divpD mulpK. Qed. Lemma divpp d : d != 0 -> d %/ d = 1. Proof. @@ -2962,9 +3025,7 @@ by rewrite -size_poly_gt0; apply: leq_trans srd. Qed. Lemma modp_mul p q m : (p * (q %% m)) %% m = (p * q) %% m. -Proof. -by rewrite [in RHS](divp_eq q m) mulrDr modp_add mulrA modp_mull add0r. -Qed. +Proof. by rewrite [in RHS](divp_eq q m) mulrDr modpD mulrA modp_mull add0r. Qed. Lemma dvdpP p q : reflect (exists qq, p = qq * q) (q %| p). Proof. @@ -3131,6 +3192,31 @@ End FieldMap. End FieldDivision. +Notation "@ 'modp_scalel'" := + (deprecate modp_scalel modpZl) (at level 10, only parsing) : fun_scope. +Notation "@ 'modp_scaler'" := + (deprecate modp_scaler modpZr) (at level 10, only parsing) : fun_scope. +Notation "@ 'modp_opp'" := + (deprecate modp_opp modpN) (at level 10, only parsing) : fun_scope. +Notation "@ 'modp_add'" := + (deprecate modp_add modpD) (at level 10, only parsing) : fun_scope. +Notation "@ 'divp_scalel'" := + (deprecate modp_scalel divpZl) (at level 10, only parsing) : fun_scope. +Notation "@ 'divp_scaler'" := + (deprecate modp_scaler divpZr) (at level 10, only parsing) : fun_scope. +Notation "@ 'divp_opp'" := + (deprecate modp_opp divpN) (at level 10, only parsing) : fun_scope. +Notation "@ 'divp_add'" := + (deprecate modp_add divpD) (at level 10, only parsing) : fun_scope. +Notation modp_scalel := (@modp_scalel _) (only parsing). +Notation modp_scaler := (@modp_scaler _ _) (only parsing). +Notation modp_opp := (@modp_opp _) (only parsing). +Notation modp_add := (@modp_add _) (only parsing). +Notation divp_scalel := (@divp_scalel _) (only parsing). +Notation divp_scaler := (@divp_scaler _ _) (only parsing). +Notation divp_opp := (@divp_opp _) (only parsing). +Notation divp_add := (@divp_add _) (only parsing). + End Field. Module ClosedField. diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v index 5680a24..b449d66 100644 --- a/mathcomp/algebra/ssralg.v +++ b/mathcomp/algebra/ssralg.v @@ -4693,7 +4693,7 @@ Lemma natf_neq0 n : (n%:R != 0 :> R) = [char R]^'.-nat n. Proof. have [-> | /prod_prime_decomp->] := posnP n; first by rewrite eqxx. rewrite !big_seq; elim/big_rec: _ => [|[p e] s /=]; first by rewrite oner_eq0. -case/mem_prime_decomp=> p_pr _ _; rewrite pnat_mul pnat_exp eqn0Ngt orbC => <-. +case/mem_prime_decomp=> p_pr _ _; rewrite pnatM pnatX eqn0Ngt orbC => <-. by rewrite natrM natrX mulf_eq0 expf_eq0 negb_or negb_and pnatE ?inE p_pr. Qed. diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v index f54a957..6d7899b 100644 --- a/mathcomp/algebra/ssrint.v +++ b/mathcomp/algebra/ssrint.v @@ -1005,24 +1005,17 @@ Lemma expr1z x : x ^ 1 = x. Proof. by []. Qed. Lemma exprN1 x : x ^ (-1) = x^-1. Proof. by []. Qed. Lemma invr_expz x n : (x ^ n)^-1 = x ^ (- n). -Proof. -by case: (intP n)=> // [|m]; rewrite ?opprK ?expr0z ?invr1 // invrK. -Qed. +Proof. by case: (intP n)=> // [|m]; rewrite ?opprK ?expr0z ?invr1 // invrK. Qed. Lemma exprz_inv x n : (x^-1) ^ n = x ^ (- n). -Proof. -by case: (intP n)=> // m; rewrite -[_ ^ (- _)]exprVn ?opprK ?invrK. -Qed. +Proof. by case: (intP n)=> // m; rewrite -[_ ^ (- _)]exprVn ?opprK ?invrK. Qed. Lemma exp1rz n : 1 ^ n = 1 :> R. -Proof. -by case: (intP n)=> // m; rewrite -?exprz_inv ?invr1; apply: expr1n. -Qed. +Proof. by case: (intP n)=> // m; rewrite -?exprz_inv ?invr1; apply: expr1n. Qed. Lemma exprSz x (n : nat) : x ^ n.+1 = x * x ^ n. Proof. exact: exprS. Qed. -Lemma exprSzr x (n : nat) : x ^ n.+1 = x ^ n * x. -Proof. exact: exprSr. Qed. +Lemma exprSzr x (n : nat) : x ^ n.+1 = x ^ n * x. Proof. exact: exprSr. Qed. Fact exprzD_nat x (m n : nat) : x ^ (m%:Z + n) = x ^ m * x ^ n. Proof. exact: exprD. Qed. @@ -1682,7 +1675,7 @@ Proof. wlog le_n21: n1 n2 / n2 <= n1. move=> IH; case/orP: (leq_total n2 n1) => /IH //. by rewrite (addnC (n2 ^ 2)) (mulnC n2) distnC. -by rewrite distnEl ?sqrn_sub ?subnK ?nat_Cauchy. +by rewrite distnEl ?sqrnB ?subnK ?nat_Cauchy. Qed. End Distn. @@ -1718,11 +1711,8 @@ Implicit Types p q r : {poly R}. Lemma coefMrz : forall p n i, (p *~ n)`_i = (p`_i *~ n). Proof. by move=> p [] n i; rewrite ?NegzE (coefMNn, coefMn). Qed. -Lemma polyC_mulrz : forall n, {morph (@polyC R) : c / c *~ n}. -Proof. -move=> [] n c; rewrite ?NegzE -?pmulrn ?polyC_muln //. -by rewrite polyC_opp mulrNz polyC_muln nmulrn. -Qed. +Lemma polyCMz : forall n, {morph (@polyC R) : c / c *~ n}. +Proof. by case/intP => // n c; rewrite ?mulrNz -!pmulrn ?polyCN ?polyCMn. Qed. Lemma hornerMz : forall n (p : {poly R}) x, (p *~ n).[x] = p.[x] *~ n. Proof. by case=> *; rewrite ?NegzE ?mulNzr ?(hornerN, hornerMn). Qed. @@ -1740,7 +1730,7 @@ Section PolyZintOIdom. Variable R : realDomainType. Lemma mulpz (p : {poly R}) (n : int) : p *~ n = n%:~R *: p. -Proof. by rewrite -[p *~ n]mulrzl -mul_polyC polyC_mulrz polyC1. Qed. +Proof. by rewrite -[p *~ n]mulrzl -mul_polyC polyCMz polyC1. Qed. End PolyZintOIdom. @@ -1787,3 +1777,7 @@ Lemma rpredXsign R S (divS : @divrPred R S) (kS : keyed_pred divS) n x : Proof. by rewrite -signr_odd; case: (odd n); rewrite ?rpredV. Qed. End rpred. + +Notation "@ 'polyC_mulrz'" := + (deprecate polyC_mulrz polyCMz) (at level 10, only parsing) : fun_scope. +Notation polyC_mulrz := (@polyC_mulrz _) (only parsing). diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v index 21394bd..462f8ad 100644 --- a/mathcomp/algebra/vector.v +++ b/mathcomp/algebra/vector.v @@ -1491,7 +1491,7 @@ move=> eq_fg; apply/vspaceP=> y. by apply/memv_imgP/memv_imgP=> [][x Vx ->]; exists x; rewrite ?eq_fg. Qed. -Lemma limg_add f : {morph lfun_img f : U V / U + V}%VS. +Lemma limgD f : {morph lfun_img f : U V / U + V}%VS. Proof. move=> U V; apply/eqP; rewrite unlock eqEsubv /subsetv /= -genmx_adds. by rewrite !genmxE !(eqmxMr _ (genmxE _)) !addsmxMr submx_refl. @@ -1499,7 +1499,7 @@ Qed. Lemma limg_sum f I r (P : pred I) Us : (f @: (\sum_(i <- r | P i) Us i) = \sum_(i <- r | P i) f @: Us i)%VS. -Proof. exact: (big_morph _ (limg_add f) (limg0 f)). Qed. +Proof. exact: (big_morph _ (limgD f) (limg0 f)). Qed. Lemma limg_cap f U V : (f @: (U :&: V) <= f @: U :&: f @: V)%VS. Proof. by rewrite subv_cap !limgS ?capvSl ?capvSr. Qed. @@ -1551,7 +1551,7 @@ Proof. by apply: (iffP subvP) => E x /E/eqlfunP. Qed. Lemma limg_ker_compl f U : (f @: (U :\: lker f) = f @: U)%VS. Proof. -rewrite -{2}(addv_diff_cap U (lker f)) limg_add; apply/esym/addv_idPl. +rewrite -{2}(addv_diff_cap U (lker f)) limgD; apply/esym/addv_idPl. by rewrite (subv_trans _ (sub0v _)) // subv0 -lkerE capvSr. Qed. @@ -1701,7 +1701,7 @@ Proof. by move=> sVW; rewrite addvS // limgS // capvS. Qed. Lemma lpreimK f W : (W <= limg f)%VS -> (f @: (f @^-1: W))%VS = W. Proof. -move=> sWf; rewrite limg_add (capv_idPl sWf) // -limg_comp. +move=> sWf; rewrite limgD (capv_idPl sWf) // -limg_comp. have /eqP->: (f @: lker f == 0)%VS by rewrite -lkerE. have /andP[/eqP defW _] := vbasisP W; rewrite addv0 -defW limg_span. rewrite map_id_in // => x Xx; rewrite lfunE /= limg_lfunVK //. @@ -2044,3 +2044,7 @@ by apply/ffunP=> i; rewrite (lfunE (Linear lhsZ)) !ffunE sol_u. Qed. End Solver. + +Notation "@ 'limg_add'" := + (deprecate limg_add limgD) (at level 10, only parsing) : fun_scope. +Notation limg_add := (@limg_add _ _ _) (only parsing). diff --git a/mathcomp/algebra/zmodp.v b/mathcomp/algebra/zmodp.v index 015d971..505fda9 100644 --- a/mathcomp/algebra/zmodp.v +++ b/mathcomp/algebra/zmodp.v @@ -142,7 +142,7 @@ Proof. by move=> Ux; rewrite /= Zp_mulC Zp_mulVz. Qed. Lemma Zp_intro_unit x y : Zp_mul y x = Zp1 -> coprime p x. Proof. case=> yx1; have:= coprimen1 p. -by rewrite -coprime_modr -yx1 coprime_modr coprime_mulr; case/andP. +by rewrite -coprime_modr -yx1 coprime_modr coprimeMr; case/andP. Qed. Lemma Zp_inv_out x : ~~ coprime p x -> Zp_inv x = x. diff --git a/mathcomp/character/inertia.v b/mathcomp/character/inertia.v index 76535fa..29d7162 100644 --- a/mathcomp/character/inertia.v +++ b/mathcomp/character/inertia.v @@ -1492,7 +1492,7 @@ have kerN_mu_t: N \subset cfker (mu / 'chi_t)%R. by rewrite /= uNlam tNlam divrr ?lin_char_unitr ?cfker_cfun1. have co_e_mu_t: coprime e #[(mu / 'chi_t)%R]%CF. suffices dv_o_mu_t: #[(mu / 'chi_t)%R]%CF %| 'o(mu)%CF * 'o('chi_t)%CF. - by rewrite (coprime_dvdr dv_o_mu_t) // coprime_mulr o_mu co_e_lam. + by rewrite (coprime_dvdr dv_o_mu_t) // coprimeMr o_mu co_e_lam. rewrite !cfDet_order_lin //; apply/dvdn_cforderP=> x Gx. rewrite invr_lin_char // !cfunE exprMn -rmorphX {2}mulnC. by rewrite !(dvdn_cforderP _) ?conjC1 ?mulr1 // dvdn_mulr. @@ -1513,7 +1513,7 @@ Corollary extend_solvable_coprime_irr G N t (theta := 'chi[N]_t) : d = c]. Proof. set e := #|G : N|; set f := truncC _ => nsNG solG IGtheta. -rewrite coprime_mulr => /andP[co_e_th co_e_f]. +rewrite coprimeMr => /andP[co_e_th co_e_f]. have [sNG nNG] := andP nsNG; pose lambda := cfDet theta. have lin_lam: lambda \is a linear_char := cfDet_lin_char theta. have IGlam: G \subset 'I[lambda]. diff --git a/mathcomp/character/integral_char.v b/mathcomp/character/integral_char.v index c603f91..c82202b 100644 --- a/mathcomp/character/integral_char.v +++ b/mathcomp/character/integral_char.v @@ -341,7 +341,7 @@ have p_dvd_supp_g i: ~~ p_dv1 i && (i != 0) -> 'chi_i g = 0. rewrite fful_i subG1 -(isog_eq1 (isog_center (quotient1_isog G))) /=. by rewrite trivZ. rewrite coprime_degree_support_cfcenter ?trivZi ?inE //. - by rewrite -/m Dm irr1_degree natCK coprime_sym coprime_expl. + by rewrite -/m Dm irr1_degree natCK coprime_sym coprimeXl. pose alpha := \sum_(i | p_dv1 i && (i != 0)) 'chi_i 1%g / p%:R * 'chi_i g. have nz_p: p%:R != 0 :> algC by rewrite pnatr_eq0 -lt0n prime_gt0. have Dalpha: alpha = - 1 / p%:R. @@ -592,7 +592,7 @@ have ZchiP: 'Res[P] 'chi_i \in 'CF(P, P :&: 'Z(G)). apply/cfun_onP=> x; rewrite inE; have [Px | /cfun0->//] := boolP (x \in P). rewrite /= -(cfcenter_fful_irr fful_i) cfResE //. apply: coprime_degree_support_cfcenter. - rewrite Dchi1 coprime_expl // prime_coprime // -p'natE //. + rewrite Dchi1 coprimeXl // prime_coprime // -p'natE //. apply: pnat_dvd p'PiG; rewrite -index_cent1 indexgS // subsetI sPG. by rewrite sub_cent1 (subsetP cPP). have /andP[_ nZG] := center_normal G; have nZP := subset_trans sPG nZG. diff --git a/mathcomp/character/mxabelem.v b/mathcomp/character/mxabelem.v index 92470d9..949ded3 100644 --- a/mathcomp/character/mxabelem.v +++ b/mathcomp/character/mxabelem.v @@ -469,7 +469,7 @@ Local Notation rVn := 'rV['F_p](gval E). Lemma dim_abelemE : n = logn p #|E|. Proof. rewrite /n'; have [_ _ [k ->]] := pgroup_pdiv pE ntE. -by rewrite /pdiv primes_exp ?primes_prime // pfactorK. +by rewrite /pdiv primesX ?primes_prime // pfactorK. Qed. Lemma card_abelem_rV : #|rVn| = #|E|. diff --git a/mathcomp/character/mxrepresentation.v b/mathcomp/character/mxrepresentation.v index 51d28f8..e94e69f 100644 --- a/mathcomp/character/mxrepresentation.v +++ b/mathcomp/character/mxrepresentation.v @@ -4908,8 +4908,7 @@ Proof. rewrite map_kermx //; congr (kermx _); apply: map_lin1_mx => //= v. rewrite map_mxvec map_mxM; congr (mxvec (_ *m _)); last first. by apply: map_lin1_mx => //= u; rewrite map_mxM map_vec_mx. -apply/row_matrixP=> i. -by rewrite -map_row !rowK map_mxvec map_mx_sub map_mx1. +by apply/row_matrixP=> i; rewrite -map_row !rowK map_mxvec map_mxB map_mx1. Qed. Lemma rcent_map A : rcent rGf A^f = rcent rG A. @@ -4990,7 +4989,7 @@ rewrite {1}in_submodE mulmxA -in_submodE -in_submodJ; last first. by rewrite genmxE -(in_factmod_addsK _ V^f) submxMr. congr (in_submod _ _); rewrite -in_factmodJ // in_factmodE mulmxA -in_factmodE. apply/eqP; rewrite -subr_eq0 -def_rGf -!map_mxM -linearB in_factmod_eq0. -rewrite -map_mx_sub map_submx -in_factmod_eq0 linearB. +rewrite -map_mxB map_submx -in_factmod_eq0 linearB. rewrite /= (in_factmodJ modU) // val_factmodK. rewrite [valUV]val_factmodE mulmxA -val_factmodE val_factmodK. rewrite -val_submodE in_submodK ?subrr //. diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v index d8ad524..a950ecc 100644 --- a/mathcomp/field/algebraics_fundamentals.v +++ b/mathcomp/field/algebraics_fundamentals.v @@ -160,7 +160,7 @@ have [n ub_n]: {n | forall y, root q y -> `|y| < n}. have [n1 ub_n1] := monic_Cauchy_bound mon_q. have /monic_Cauchy_bound[n2 ub_n2]: (-1) ^+ d *: (q \Po - 'X) \is monic. rewrite monicE lead_coefZ lead_coef_comp ?size_opp ?size_polyX // -/d. - by rewrite lead_coef_opp lead_coefX (monicP mon_q) (mulrC 1) signrMK. + by rewrite lead_coefN lead_coefX (monicP mon_q) (mulrC 1) signrMK. exists (Num.max n1 n2) => y; rewrite ltNge ler_normr !leUx rootE. apply: contraL => /orP[]/andP[] => [/ub_n1/gt_eqF->// | _ /ub_n2/gt_eqF]. by rewrite hornerZ horner_comp !hornerE opprK mulf_eq0 signr_eq0 => /= ->. @@ -171,7 +171,7 @@ right=> [[y Dx]]; case: xa'x; exists y => //. have{x Dx qx0} qy0: root q y by rewrite Dx fmorph_root in qx0. have /dvdzP[b Da]: (denq y %| a)%Z. have /Gauss_dvdzl <-: coprimez (denq y) (numq y ^+ d). - by rewrite coprimez_sym coprimez_expl //; apply: coprime_num_den. + by rewrite coprimez_sym coprimezXl //; apply: coprime_num_den. pose p1 : {poly int} := a *: 'X^d - p. have Dp1: p1 ^ intr = a%:~R *: ('X^d - q). by rewrite rmorphB linearZ /= map_polyXn scalerBr Dq scalerKV ?intr_eq0. @@ -231,7 +231,7 @@ without loss mon_q: q nCq q_dv_p / q \is monic. move=> IHq; pose a := lead_coef q; pose q1 := a^-1 *: q. have nz_a: a != 0 by rewrite lead_coef_eq0 (dvdpN0 q_dv_p) ?monic_neq0. have /IHq IHq1: q1 \is monic by rewrite monicE lead_coefZ mulVf. - by rewrite -IHq1 ?size_scale ?dvdp_scalel ?invr_eq0. + by rewrite -IHq1 ?size_scale ?dvdpZl ?invr_eq0. without loss{nCq} qx0: q mon_q q_dv_p / root (q ^ FtoL) x. have /dvdpP[q1 Dp] := q_dv_p; rewrite DpI Dp rmorphM rootM -implyNb in pIx0. have mon_q1: q1 \is monic by rewrite Dp monicMr in mon_p. @@ -515,7 +515,7 @@ have add_Rroot xR p c: {yR | extendsR xR yR & has_Rroot xR p c -> root_in yR p}. have ab_le m n: (m <= n)%N -> (ab_ n).2 \in Iab_ m. move/subnKC=> <-; move: {n}(n - m)%N => n; rewrite /ab_. have /(findP m)[/(findP n)[[_ _]]] := xab0. - rewrite /find -iter_add -!/(find _ _) -!/(ab_ _) addnC !inE. + rewrite /find -iterD -!/(find _ _) -!/(ab_ _) addnC !inE. by move: (ab_ _) => /= ab_mn le_ab_mn [/le_trans->]. pose lt v w := 0 < nlim (w - v) (n_ (w - v)). have posN v: lt 0 (- v) = lt v 0 by rewrite /lt subr0 add0r. @@ -723,7 +723,7 @@ have /all_sig[n_ FTA] z: {n | z \in sQ (z_ n)}. have mon_p: p \is monic. have mon_pw: pw \is monic := monic_minPoly _ _. rewrite map_monic mulNr -mulrN monicMl // monicE. - rewrite !(lead_coef_opp, lead_coef_comp) ?size_opp ?size_polyX //. + rewrite !(lead_coefN, lead_coef_comp) ?size_opp ?size_polyX //. by rewrite lead_coefX sz_pw -signr_odd odd_2'nat oddPG mulrN1 opprK. have Dp0: p.[0] = - ofQ t pw.[0] ^+ 2. rewrite -(rmorph0 (ofQ t)) horner_map hornerM rmorphM. diff --git a/mathcomp/field/closed_field.v b/mathcomp/field/closed_field.v index a6f7514..266788c 100644 --- a/mathcomp/field/closed_field.v +++ b/mathcomp/field/closed_field.v @@ -200,7 +200,7 @@ Lemma eval_sumpT (p q : polyF) (e : seq F) : Proof. elim: p q => [|a p Hp] q /=; first by rewrite add0r. case: q => [|b q] /=; first by rewrite addr0. -rewrite Hp mulrDl -!addrA; congr (_ + _); rewrite polyC_add addrC -addrA. +rewrite Hp mulrDl -!addrA; congr (_ + _); rewrite polyCD addrC -addrA. by congr (_ + _); rewrite addrC. Qed. @@ -220,15 +220,12 @@ Lemma eval_mulpT (p q : polyF) (e : seq F) : Proof. elim: p q=> [|a p Hp] q /=; first by rewrite mul0r. rewrite eval_sumpT /= Hp addr0 mulrDl addrC mulrAC; congr (_ + _). -elim: q=> [|b q Hq] /=; first by rewrite mulr0. -by rewrite Hq polyC_mul mulrDr mulrA. +by elim: q=> [|b q Hq] /=; rewrite ?mulr0 // Hq polyCM mulrDr mulrA. Qed. Lemma rpoly_map_mul (t : tF) (p : polyF) (rt : rterm t) : rpoly [seq (t * x)%T | x <- p] = rpoly p. -Proof. -by rewrite /rpoly all_map /= (@eq_all _ _ (@rterm _)) // => x; rewrite /= rt. -Qed. +Proof. by rewrite /rpoly all_map; apply/eq_all => x; rewrite /= rt. Qed. Lemma rmulpT (p q : polyF) : rpoly p -> rpoly q -> rpoly (mulpT p q). Proof. @@ -242,7 +239,7 @@ Definition opppT : polyF -> polyF := map (GRing.Mul (- 1%T)%T). Lemma eval_opppT (p : polyF) (e : seq F) : eval_poly e (opppT p) = - eval_poly e p. Proof. -by elim: p; rewrite /= ?oppr0 // => ? ? ->; rewrite !mulNr opprD polyC_opp mul1r. +by elim: p; rewrite /= ?oppr0 // => ? ? ->; rewrite !mulNr opprD polyCN mul1r. Qed. Definition natmulpT n : polyF -> polyF := map (GRing.Mul n%:R%T). @@ -251,7 +248,7 @@ Lemma eval_natmulpT (p : polyF) (n : nat) (e : seq F) : eval_poly e (natmulpT n p) = (eval_poly e p) *+ n. Proof. elim: p; rewrite //= ?mul0rn // => c p ->. -rewrite mulrnDl mulr_natl polyC_muln; congr (_ + _). +rewrite mulrnDl mulr_natl polyCMn; congr (_ + _). by rewrite -mulr_natl mulrAC -mulrA mulr_natl mulrC. Qed. diff --git a/mathcomp/field/cyclotomic.v b/mathcomp/field/cyclotomic.v index 658258c..5359cce 100644 --- a/mathcomp/field/cyclotomic.v +++ b/mathcomp/field/cyclotomic.v @@ -50,10 +50,9 @@ End Ring. Lemma separable_Xn_sub_1 (R : idomainType) n : n%:R != 0 :> R -> @separable_poly R ('X^n - 1). Proof. -case: n => [/eqP// | n nz_n]; rewrite /separable_poly linearB /=. -rewrite derivC subr0 derivXn -scaler_nat coprimep_scaler //= exprS -scaleN1r. -rewrite coprimep_sym coprimep_addl_mul coprimep_scaler ?coprimep1 //. -by rewrite (signr_eq0 _ 1). +case: n => [/eqP// | n nz_n]; rewrite /separable_poly linearB /= derivC subr0. +rewrite derivXn -scaler_nat coprimepZr //= exprS -scaleN1r coprimep_sym. +by rewrite coprimep_addl_mul coprimepZr ?coprimep1 // (signr_eq0 _ 1). Qed. Section Field. @@ -188,7 +187,7 @@ have injf: injective (f e). rewrite modnMml -mulnA -modnMmr -{1}(mul1n e). by rewrite (chinese_modr co_e_n 0) modnMmr muln1 modn_small. rewrite [_ n](reindex_inj injf); apply: eq_big => k /=. - by rewrite coprime_modl coprime_mull co_e_n andbT. + by rewrite coprime_modl coprimeMl co_e_n andbT. by rewrite prim_expr_mod // mulnC exprM -Dz0. Qed. @@ -269,7 +268,7 @@ have [|k_gt1] := leqP k 1; last have [p p_pr /dvdnP[k1 Dk]] := pdivP k_gt1. rewrite k0 /coprime gcd0n in cokn; rewrite (eqP cokn). rewrite -(size_map_inj_poly (can_inj intCK)) // -Df -Dpf. by rewrite -(subnKC g_gt1) -(subnKC (size_minCpoly z)) !addnS. -move: cokn; rewrite Dk coprime_mull => /andP[cok1n]. +move: cokn; rewrite Dk coprimeMl => /andP[cok1n]. rewrite prime_coprime // (dvdn_charf (char_Fp p_pr)) => /co_fg {co_fg}. have charFpX: p \in [char {poly 'F_p}]. by rewrite (rmorph_char (polyC_rmorphism _)) ?char_Fp. diff --git a/mathcomp/field/falgebra.v b/mathcomp/field/falgebra.v index bdff38a..db235fe 100644 --- a/mathcomp/field/falgebra.v +++ b/mathcomp/field/falgebra.v @@ -1173,11 +1173,11 @@ by rewrite -aimgM limgS // [rhs in (_ <= rhs)%VS]agenvEl addvSr. Qed. Lemma aimg_adjoin (f : ahom aT rT) U x : (f @: <<U; x>> = <<f @: U; f x>>)%VS. -Proof. by rewrite aimg_agen limg_add limg_line. Qed. +Proof. by rewrite aimg_agen limgD limg_line. Qed. Lemma aimg_adjoin_seq (f : ahom aT rT) U xs : (f @: <<U & xs>> = <<f @: U & map f xs>>)%VS. -Proof. by rewrite aimg_agen limg_add limg_span. Qed. +Proof. by rewrite aimg_agen limgD limg_span. Qed. Fact ker_sub_ahom_is_aspace (f g : ahom aT rT) : is_aspace (lker (ahval f - ahval g)). diff --git a/mathcomp/field/fieldext.v b/mathcomp/field/fieldext.v index df7ef5a..d99b69b 100644 --- a/mathcomp/field/fieldext.v +++ b/mathcomp/field/fieldext.v @@ -1290,8 +1290,8 @@ Qed. Fact mulfx_addl : left_distributive subfext_mul subfext_add. Proof. -elim/quotW=> x; elim/quotW=> y; elim/quotW=> w; rewrite !piE /subfx_mul_rep. -by rewrite linearD /= mulrDl modp_add linearD. +elim/quotW=> x; elim/quotW=> y; elim/quotW=> w. +by rewrite !piE /subfx_mul_rep linearD /= mulrDl modpD linearD. Qed. Fact nonzero1fx : subfext1 != subfext0. @@ -1378,7 +1378,7 @@ Definition subfx_root := subfx_eval 'X. Lemma subfx_eval_is_rmorphism : rmorphism subfx_eval. Proof. do 2?split=> [x y|] /=; apply/eqP; rewrite piE. -- by rewrite -linearB modp_add modNp. +- by rewrite -linearB modpD modNp. - by rewrite /subfx_mul_rep !poly_rV_modp_K !(modp_mul, mulrC _ y). by rewrite modp_small // size_poly1 -subn_gt0 subn1. Qed. @@ -1529,7 +1529,7 @@ suffices [L dimL [toPF [toL toPF_K toL_K]]]: elim/poly_ind: q => [|a q IHq]. by rewrite map_poly0 horner0 linear0 mod0p. rewrite rmorphD rmorphM /= map_polyX map_polyC hornerMXaddC linearD /=. - rewrite linearZ /= -(rmorph1 toL) toL_K -modp_scalel alg_polyC modp_add. + rewrite linearZ /= -(rmorph1 toL) toL_K -modpZl alg_polyC modpD. congr (_ + _); rewrite -toL_K rmorphM /= -/z; congr (toPF (_ * z)). by apply: (can_inj toPF_K); rewrite toL_K. pose toL q : vL := poly_rV (q %% p); pose toPF (x : vL) := rVpoly x. @@ -1547,13 +1547,13 @@ have mul1: left_id L1 mul. by move=> x; apply: toPinj; rewrite mulC !toL_K modp_mul mulr1 -toL_K toPF_K. have mulD: left_distributive mul +%R. move=> x y z; apply: toPinj; rewrite /toPF raddfD /= -!/(toPF _). - by rewrite !toL_K /toPF raddfD mulrDl modp_add. + by rewrite !toL_K /toPF raddfD mulrDl modpD. have nzL1: L1 != 0 by rewrite -(inj_eq toPinj) L1K /toPF raddf0 oner_eq0. pose mulM := ComRingMixin mulA mulC mul1 mulD nzL1. pose rL := ComRingType (RingType vL mulM) mulC. have mulZl: GRing.Lalgebra.axiom mul. - move=> a x y; apply: toPinj; rewrite toL_K /toPF !linearZ /= -!/(toPF _). - by rewrite toL_K -scalerAl modp_scalel. + move=> a x y; apply: toPinj. + by rewrite toL_K /toPF !linearZ /= -!/(toPF _) toL_K -scalerAl modpZl. have mulZr: GRing.Algebra.axiom (LalgType F rL mulZl). by move=> a x y; rewrite !(mulrC x) scalerAl. pose aL := AlgType F _ mulZr; pose urL := FalgUnitRingType aL. @@ -1567,7 +1567,7 @@ have unitE: GRing.Field.mixin_of urL. rewrite dvdp_gcdl -ltnNge /= => /eqp_size->. by rewrite (polySpred nz_p) ltnS size_poly. suffices: x * toL u.2 = 1 by exists (toL u.2); rewrite mulrC. - apply: toPinj; rewrite !toL_K -upq1 modp_mul modp_add mulrC. + apply: toPinj; rewrite !toL_K -upq1 modp_mul modpD mulrC. by rewrite modp_mull add0r. pose ucrL := [comUnitRingType of ComRingType urL mulC]. have mul0 := GRing.Field.IdomainMixin unitE. @@ -1575,8 +1575,7 @@ pose fL := FieldType (IdomainType ucrL mul0) unitE. exists [fieldExtType F of faL for fL]; first by rewrite dimvf; apply: mul1n. exists [linear of toPF as rVpoly]. suffices toLM: lrmorphism (toL : {poly F} -> aL) by exists (LRMorphism toLM). -have toLlin: linear toL. - by move=> a q1 q2; rewrite -linearP -modp_scalel -modp_add. +have toLlin: linear toL by move=> a q1 q2; rewrite -linearP -modpZl -modpD. do ?split; try exact: toLlin; move=> q r /=. by apply: toPinj; rewrite !toL_K modp_mul -!(mulrC r) modp_mul. Qed. @@ -1607,13 +1606,13 @@ have mul1: left_id L1 mul. by rewrite size_poly. have mulD: left_distributive mul +%R. move=> x y z; apply: canLR rVpolyK _. - by rewrite !raddfD mulrDl /= !toL_K /toL modp_add. + by rewrite !raddfD mulrDl /= !toL_K /toL modpD. have nzL1: L1 != 0 by rewrite -(can_eq rVpolyK) L1K raddf0 oner_eq0. pose mulM := ComRingMixin mulA mulC mul1 mulD nzL1. pose rL := ComRingType (RingType vL mulM) mulC. have mulZl: GRing.Lalgebra.axiom mul. - move=> a x y; apply: canRL rVpolyK _; rewrite !linearZ /= toL_K. - by rewrite -scalerAl modp_scalel. + move=> a x y; apply: canRL rVpolyK _. + by rewrite !linearZ /= toL_K -scalerAl modpZl. have mulZr: @GRing.Algebra.axiom _ (LalgType F rL mulZl). by move=> a x y; rewrite !(mulrC x) scalerAl. pose aL := AlgType F _ mulZr; pose urL := FalgUnitRingType aL. @@ -1638,7 +1637,7 @@ have q_z q: rVpoly (map_poly iota q).[z] = q %% p. elim/poly_ind: q => [|a q IHq]. by rewrite map_poly0 horner0 linear0 mod0p. rewrite rmorphD rmorphM /= map_polyX map_polyC hornerMXaddC linearD /=. - rewrite linearZ /= L1K alg_polyC modp_add; congr (_ + _); last first. + rewrite linearZ /= L1K alg_polyC modpD; congr (_ + _); last first. by rewrite modp_small // size_polyC; case: (~~ _) => //; apply: ltnW. by rewrite !toL_K IHq mulrC modp_mul mulrC modp_mul. exists z; first by rewrite /root -(can_eq rVpolyK) q_z modpp linear0. diff --git a/mathcomp/field/separable.v b/mathcomp/field/separable.v index bc2eecb..e51a660 100644 --- a/mathcomp/field/separable.v +++ b/mathcomp/field/separable.v @@ -68,13 +68,13 @@ apply: (iffP idP) => [sep_p | [sq'p nz_der1p]]. split=> [u v | u u_dv_p]; last first. apply: contraTneq => u'0; rewrite -leqNgt -(eqnP sep_p). rewrite dvdp_leq -?size_poly_eq0 ?(eqnP sep_p) // dvdp_gcd u_dv_p. - have /dvdp_scaler <-: lead_coef u ^+ scalp p u != 0 by rewrite lcn_neq0. + have /dvdpZr <-: lead_coef u ^+ scalp p u != 0 by rewrite lcn_neq0. by rewrite -derivZ -Pdiv.Idomain.divpK //= derivM u'0 mulr0 addr0 dvdp_mull. rewrite Pdiv.Idomain.dvdp_eq mulrCA mulrA; set c := _ ^+ _ => /eqP Dcp. have nz_c: c != 0 by rewrite lcn_neq0. - move: sep_p; rewrite coprimep_sym -[separable _](coprimep_scalel _ _ nz_c). - rewrite -(coprimep_scaler _ _ nz_c) -derivZ Dcp derivM coprimep_mull. - by rewrite coprimep_addl_mul !coprimep_mulr -andbA => /and4P[]. + move: sep_p; rewrite coprimep_sym -[separable _](coprimepZl _ _ nz_c). + rewrite -(coprimepZr _ _ nz_c) -derivZ Dcp derivM coprimepMl. + by rewrite coprimep_addl_mul !coprimepMr -andbA => /and4P[]. rewrite /separable coprimep_def eqn_leq size_poly_gt0; set g := gcdp _ _. have nz_g: g != 0. rewrite -dvd0p dvdp_gcd -(mulr0 0); apply/nandP; left. @@ -82,9 +82,9 @@ have nz_g: g != 0. have [g_p]: g %| p /\ g %| p^`() by rewrite dvdp_gcdr ?dvdp_gcdl. pose c := lead_coef g ^+ scalp p g; have nz_c: c != 0 by rewrite lcn_neq0. have Dcp: c *: p = p %/ g * g by rewrite Pdiv.Idomain.divpK. -rewrite nz_g andbT leqNgt -(dvdp_scaler _ _ nz_c) -derivZ Dcp derivM. +rewrite nz_g andbT leqNgt -(dvdpZr _ _ nz_c) -derivZ Dcp derivM. rewrite dvdp_addr; last by rewrite dvdp_mull. -rewrite Gauss_dvdpr; last by rewrite sq'p // mulrC -Dcp dvdp_scalel. +rewrite Gauss_dvdpr; last by rewrite sq'p // mulrC -Dcp dvdpZl. by apply: contraL => /nz_der1p nz_g'; rewrite gtNdvdp ?nz_g' ?lt_size_deriv. Qed. @@ -114,8 +114,8 @@ Proof. apply/idP/and3P => [sep_pq | [sep_p seq_q co_pq]]. rewrite !(dvdp_separable _ sep_pq) ?dvdp_mulIr ?dvdp_mulIl //. by rewrite (separable_coprime sep_pq). -rewrite /separable derivM coprimep_mull {1}addrC mulrC !coprimep_addl_mul. -by rewrite !coprimep_mulr (coprimep_sym q p) co_pq !andbT; apply/andP. +rewrite /separable derivM coprimepMl {1}addrC mulrC !coprimep_addl_mul. +by rewrite !coprimepMr (coprimep_sym q p) co_pq !andbT; apply/andP. Qed. Lemma eqp_separable p q : p %= q -> separable p = separable q. @@ -145,10 +145,10 @@ split=> [|u u_pg u_gt1]; last first. apply/eqP=> u'0 /=; have [k /negP[]] := max_dvd_u u u_gt1. elim: k => [|k IHk]; first by rewrite dvd1p. suffices: u ^+ k.+1 %| (p %/ g) * g. - by rewrite Pdiv.Idomain.divpK ?dvdp_gcdl // dvdp_scaler ?lcn_neq0. + by rewrite Pdiv.Idomain.divpK ?dvdp_gcdl // dvdpZr ?lcn_neq0. rewrite exprS dvdp_mul // dvdp_gcd IHk //=. suffices: u ^+ k %| (p %/ u ^+ k * u ^+ k)^`(). - by rewrite Pdiv.Idomain.divpK // derivZ dvdp_scaler ?lcn_neq0. + by rewrite Pdiv.Idomain.divpK // derivZ dvdpZr ?lcn_neq0. by rewrite !derivCE u'0 mul0r mul0rn mulr0 addr0 dvdp_mull. have pg_dv_p: p %/ g %| p by rewrite divp_dvd ?dvdp_gcdl. apply/poly_square_freeP=> u; rewrite neq_ltn ltnS leqn0 size_poly_eq0. @@ -157,11 +157,11 @@ case/predU1P=> [-> | /max_dvd_u[k]]. apply: contra => u2_dv_pg; case: k; [by rewrite dvd1p | elim=> [|n IHn]]. exact: dvdp_trans (dvdp_mulr _ _) (dvdp_trans u2_dv_pg pg_dv_p). suff: u ^+ n.+2 %| (p %/ g) * g. - by rewrite Pdiv.Idomain.divpK ?dvdp_gcdl // dvdp_scaler ?lcn_neq0. + by rewrite Pdiv.Idomain.divpK ?dvdp_gcdl // dvdpZr ?lcn_neq0. rewrite -add2n exprD dvdp_mul // dvdp_gcd. rewrite (dvdp_trans _ IHn) ?exprS ?dvdp_mull //=. suff: u ^+ n %| ((p %/ u ^+ n.+1) * u ^+ n.+1)^`(). - by rewrite Pdiv.Idomain.divpK // derivZ dvdp_scaler ?lcn_neq0. + by rewrite Pdiv.Idomain.divpK // derivZ dvdpZr ?lcn_neq0. by rewrite !derivCE dvdp_add // -1?mulr_natl ?exprS !dvdp_mull. Qed. @@ -260,7 +260,7 @@ without loss{nz_q} sep_q: q qy_0 / separable_poly q. rewrite Dq rmorphM /= gcdp_map -(eqp_dvdr _ (gcdp_mul2l _ _ _)) -deriv_map Dr. rewrite dvdp_gcd derivM deriv_exp derivXsubC mul1r !mulrA dvdp_mulIr /=. rewrite mulrDr mulrA dvdp_addr ?dvdp_mulIr // exprS -scaler_nat -!scalerAr. - rewrite dvdp_scaler -?(rmorph_nat iota) ?fmorph_eq0 ?charF0 //. + rewrite dvdpZr -?(rmorph_nat iota) ?fmorph_eq0 ?charF0 //. rewrite mulrA dvdp_mul2r ?expf_neq0 ?polyXsubC_eq0 //. by rewrite Gauss_dvdpl ?dvdp_XsubCl // coprimep_sym coprimep_XsubC. have [r nz_r PETxy] := large_field_PET qy_0 sep_q. @@ -585,7 +585,7 @@ elim: n => // n IHn in x @d *; rewrite ltnS => le_d_n. have [[p charLp]|] := altP (separablePn K x); last by rewrite negbK; exists 1%N. case=> g Kg defKx; have p_pr := charf_prime charLp. suffices /IHn[m /andP[charLm sepKxpm]]: adjoin_degree K (x ^+ p) < n. - by exists (p * m)%N; rewrite pnat_mul pnatE // charLp charLm exprM. + by exists (p * m)%N; rewrite pnatM pnatE // charLp charLm exprM. apply: leq_trans le_d_n; rewrite -ltnS -!size_minPoly. have nzKx: minPoly K x != 0 by rewrite monic_neq0 ?monic_minPoly. have nzg: g != 0 by apply: contra_eqN defKx => /eqP->; rewrite comp_poly0. @@ -844,7 +844,7 @@ Lemma inseparable_add K x y : Proof. have insepP := purely_inseparable_elementP. move=> /insepP[n charLn Kxn] /insepP[m charLm Kym]; apply/insepP. -have charLnm: [char L].-nat (n * m)%N by rewrite pnat_mul charLn. +have charLnm: [char L].-nat (n * m)%N by rewrite pnatM charLn. by exists (n * m)%N; rewrite ?exprDn_char // {2}mulnC !exprM memvD // rpredX. Qed. @@ -944,7 +944,7 @@ by apply/FadjoinP/andP; rewrite sKE separable_generator_mem. Qed. Lemma separable_refl K : separable K K. -Proof. by apply/separableP; apply: base_separable. Qed. +Proof. exact/separableP/base_separable. Qed. Lemma separable_trans M K E : separable K M -> separable M E -> separable K E. Proof. @@ -986,7 +986,7 @@ Proof. have insepP := purely_inseparableP => /insepP insepK_M /insepP insepM_E. have insepPe := purely_inseparable_elementP. apply/insepP=> x /insepM_E/insepPe[n charLn /insepK_M/insepPe[m charLm Kxnm]]. -by apply/insepPe; exists (n * m)%N; rewrite ?exprM // pnat_mul charLn charLm. +by apply/insepPe; exists (n * m)%N; rewrite ?exprM // pnatM charLn charLm. Qed. End Separable. diff --git a/mathcomp/fingroup/gproduct.v b/mathcomp/fingroup/gproduct.v index 7e14ce0..cdd68fd 100644 --- a/mathcomp/fingroup/gproduct.v +++ b/mathcomp/fingroup/gproduct.v @@ -829,7 +829,7 @@ have{defGi} defGi: \big[dprod/1]_(j | Q j && (j != i)) A j = Gi. by apply: IHm => [||j /andP[/sQP]] //; rewrite (cardD1x Qi) in leQm. rewrite defGi dprodE // coprime_TIg // -defAi -(bigdprod_card defGi). elim/big_rec: _ => [|j n /andP[neq_ji Qj] IHn]; first exact: coprimen1. -by rewrite coprime_mulr coprime_sym coA ?sQP. +by rewrite coprimeMr coprime_sym coA ?sQP. Qed. Lemma mem_dprod G A B x : A \x B = G -> x \in G -> diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v index 469c649..ba26ab6 100644 --- a/mathcomp/solvable/abelian.v +++ b/mathcomp/solvable/abelian.v @@ -177,7 +177,7 @@ have [-> | nt_x] := eqVneq x 1. apply: (iffP idP) => [/eqP | [p p_pr /eqP x_pn]]. by exists (pdiv #[x]); rewrite ?pdiv_prime ?order_gt1. rewrite (@pdiv_p_elt p) //; rewrite -order_dvdn in x_pn. -by rewrite [p_elt _ _](pnat_dvd x_pn) // pnat_exp pnat_id. +by rewrite [p_elt _ _](pnat_dvd x_pn) // pnatX pnat_id. Qed. Lemma Mho_p_elt (p : nat) x : x \in A -> p.-elt x -> x ^+ (p ^ n) \in Mho. @@ -390,7 +390,7 @@ Proof. by rewrite /abelem pgroup1 abelian1 exponent1 dvd1n. Qed. Lemma abelemE p G : prime p -> p.-abelem G = abelian G && (exponent G %| p). Proof. move=> p_pr; rewrite /abelem -pnat_exponent andbA -!(andbC (_ %| _)). -by case: (dvdn_pfactor _ 1 p_pr) => // [[k _ ->]]; rewrite pnat_exp pnat_id. +by case: (dvdn_pfactor _ 1 p_pr) => // [[k _ ->]]; rewrite pnatX pnat_id. Qed. Lemma abelemP p G : @@ -2177,4 +2177,3 @@ Lemma fin_ring_char_abelem p (R : finRingType) : Proof. exact: fin_lmod_char_abelem [finLmodType R of R^o]. Qed. End FimModAbelem. - diff --git a/mathcomp/solvable/extraspecial.v b/mathcomp/solvable/extraspecial.v index 58c3cf0..2dcb1d5 100644 --- a/mathcomp/solvable/extraspecial.v +++ b/mathcomp/solvable/extraspecial.v @@ -182,7 +182,7 @@ by exists 1%R; rewrite ?inE. Qed. Lemma pX1p2_pgroup : p.-group p^{1+2}. -Proof. by rewrite /pgroup card_pX1p2 pnat_exp pnat_id. Qed. +Proof. by rewrite /pgroup card_pX1p2 pnatX pnat_id. Qed. (* This is part of the existence half of Aschbacher ex. (8.7)(1) *) Lemma pX1p2_extraspecial : extraspecial p^{1+2}. @@ -207,7 +207,7 @@ have ->: p^{1+2} = 'Ohm_1(p^{1+2}). case/existsP: (isoGrp_hom Grp_pX1p2) => [[x y]] /=. case/eqP=> <- xp yp _ _; rewrite joing_idl joing_idr genS //. by rewrite subsetI subset_gen subUset !sub1set !inE xp yp!eqxx. -rewrite exponent_Ohm1_class2 ?card_pX1p2 ?odd_exp // nil_class2. +rewrite exponent_Ohm1_class2 ?card_pX1p2 ?oddX // nil_class2. by have [[_ ->] _ ] := pX1p2_extraspecial. Qed. @@ -217,7 +217,7 @@ Lemma isog_pX1p2 (gT : finGroupType) (G : {group gT}) : Proof. move=> esG expGp oG; apply/(isoGrpP _ Grp_pX1p2). rewrite card_pX1p2; split=> //. -have pG: p.-group G by rewrite /pgroup oG pnat_exp pnat_id. +have pG: p.-group G by rewrite /pgroup oG pnatX pnat_id. have oZ := card_center_extraspecial pG esG. have [x Gx notZx]: exists2 x, x \in G & x \notin 'Z(G). apply/subsetPn; rewrite proper_subn // properEcard center_sub oZ oG. @@ -283,7 +283,7 @@ by rewrite oG oZ IHn -expnD mulKn ?prime_gt0. Qed. Lemma pX1p2n_pgroup n : prime p -> p.-group p^{1+2*n}. -Proof. by move=> p_pr; rewrite /pgroup card_pX1p2n // pnat_exp pnat_id. Qed. +Proof. by move=> p_pr; rewrite /pgroup card_pX1p2n // pnatX pnat_id. Qed. (* This is part of the existence half of Aschbacher (23.13) *) Lemma exponent_pX1p2n n : prime p -> odd p -> exponent p^{1+2*n} = p. @@ -526,7 +526,7 @@ Lemma isog_pX1p2n n (gT : finGroupType) (G : {group gT}) : Proof. move=> p_pr esG oG expG; have p_gt1 := prime_gt1 p_pr. have not_le_p3_p: ~~ (p ^ 3 <= p) by rewrite (leq_exp2l 3 1). -have pG: p.-group G by rewrite /pgroup oG pnat_exp pnat_id. +have pG: p.-group G by rewrite /pgroup oG pnatX pnat_id. have oZ := card_center_extraspecial pG esG. have{pG esG} [Es p3Es defG] := extraspecial_structure pG esG. set Z := 'Z(G) in oZ defG p3Es. @@ -614,7 +614,7 @@ by rewrite -muln_divA // mulnC -(expnD 2 2). Qed. Lemma DnQ_pgroup n : 2.-group 'D^n*Q. -Proof. by rewrite /pgroup card_DnQ pnat_exp. Qed. +Proof. by rewrite /pgroup card_DnQ pnatX. Qed. (* Final part of the existence half of Aschbacher (23.14). *) Lemma DnQ_extraspecial n : extraspecial 'D^n*Q. @@ -659,7 +659,7 @@ Proof. elim: n G => [|n IHn] G oG esG. case/negP: (extraspecial_nonabelian esG). by rewrite cyclic_abelian ?prime_cyclic ?oG. -have pG: 2.-group G by rewrite /pgroup oG pnat_exp. +have pG: 2.-group G by rewrite /pgroup oG pnatX. have oZ:= card_center_extraspecial pG esG. have: 'Z(G) \subset 'Ohm_1(G). apply/subsetP=> z Zz; rewrite (OhmE _ pG) mem_gen //. @@ -705,7 +705,7 @@ have AutZin2_1p2: Aut_in (Aut 2^{1+2}) 'Z(2^{1+2}) \isog Aut 'Z(2^{1+2}). have [isoR | isoR] := IHn R oR esR. by left; case: pX1p2S => gz isoZ; rewrite (isog_cprod_by _ defG). have n_gt0: n > 0. - have pR: 2.-group R by rewrite /pgroup oR pnat_exp. + have pR: 2.-group R by rewrite /pgroup oR pnatX. have:= min_card_extraspecial pR esR. by rewrite oR leq_exp2l // ltnS (leq_double 1). case: DnQ_P isoR => gR isoZR /=; rewrite isog_sym; case/isogP=> fR injfR im_fR. @@ -742,7 +742,7 @@ elim: n => [|n IHn]; first by rewrite p_rank_abelem ?prime_abelem ?card_pX1p2n. have oDDn: #|'D^n.+1| = (2 ^ n.+1.*2.+1)%N by apply: card_pX1p2n. have esDDn: extraspecial 'D^n.+1 by apply: pX1p2n_extraspecial. do [case: pX1p2S => gz isoZ; set DDn := [set: _]] in oDDn esDDn *. -have pDDn: 2.-group DDn by rewrite /pgroup oDDn pnat_exp. +have pDDn: 2.-group DDn by rewrite /pgroup oDDn pnatX. apply/eqP; rewrite eqn_leq; apply/andP; split. have [E EprE]:= p_rank_witness 2 [group of DDn]. have [sEDDn abelE <-] := pnElemP EprE; have [pE cEE _]:= and3P abelE. diff --git a/mathcomp/solvable/extremal.v b/mathcomp/solvable/extremal.v index 8185773..a0c40ee 100644 --- a/mathcomp/solvable/extremal.v +++ b/mathcomp/solvable/extremal.v @@ -350,7 +350,7 @@ have os: #[s] = (p ^ (n - e0))%N. case/dvdn_pfactor=> // d; rewrite leq_eqVlt. case/predU1P=> [-> // | lt_d os]; case/idPn: (p_gt1); rewrite -os0. by rewrite order_gt1 negbK -order_dvdn os dvdn_exp2l // -ltnS -subSn. -have p_s: p.-elt s by rewrite /p_elt os pnat_exp ?pnat_id. +have p_s: p.-elt s by rewrite /p_elt os pnatX ?pnat_id. have defS1: 'Ohm_1(<[s]>) = <[s0]>. apply/eqP; rewrite eq_sym eqEcard cycle_subG -orderE os0. rewrite (Ohm1_cyclic_pgroup_prime _ p_s) ?cycle_cyclic ?leqnn ?cycle_eq1 //=. @@ -398,7 +398,7 @@ Lemma extremal_generators_facts gT (G : {group gT}) p n x y : <[x]> * <[y]> = G & <[y]> \subset 'N(<[x]>)]. Proof. move=> p_pr [oG Gx ox] /setDP[Gy notXy]. -have pG: p.-group G by rewrite /pgroup oG pnat_exp pnat_id. +have pG: p.-group G by rewrite /pgroup oG pnatX pnat_id. have maxX: maximal <[x]> G. rewrite p_index_maximal -?divgS ?cycle_subG // -orderE oG ox. case: (n) oG => [|n' _]; last by rewrite -expnB ?subSnn ?leqnSn ?prime_gt0. @@ -438,7 +438,7 @@ rewrite /modular_gtype def_p def_q def_r; apply: Extremal.Grp => //. set B := <[_]>; have Bb: Zp1 \in B by apply: cycle_id. have oB: #|B| = q by rewrite -orderE order_Zp1 Zp_cast. have cycB: cyclic B by rewrite cycle_cyclic. -have pB: p.-group B by rewrite /pgroup oB pnat_exp ?pnat_id. +have pB: p.-group B by rewrite /pgroup oB pnatX ?pnat_id. have ntB: B != 1 by rewrite -cardG_gt1 oB. have [] := cyclic_pgroup_Aut_structure pB cycB ntB. rewrite oB pfactorK //= -/B -(expg_znat r.+1 Bb) oB => mB [[def_mB _ _ _ _] _]. @@ -711,7 +711,7 @@ rewrite !expnS !mulKn // -!expnS /=; set q := (2 ^ _)%N. have q_gt1: q > 1 by rewrite (ltn_exp2l 0). apply: Extremal.Grp => //; set B := <[_]>. have oB: #|B| = q by rewrite -orderE order_Zp1 Zp_cast. -have pB: 2.-group B by rewrite /pgroup oB pnat_exp. +have pB: 2.-group B by rewrite /pgroup oB pnatX. have ntB: B != 1 by rewrite -cardG_gt1 oB. have [] := cyclic_pgroup_Aut_structure pB (cycle_cyclic _) ntB. rewrite oB /= pfactorK //= -/B => m [[def_m _ _ _ _] _]. @@ -1133,7 +1133,7 @@ have def_ur: {in G, forall t, #[t] = 2 -> t = u ^+ r}. move=> t Gt /= ot; case Ut: (t \in <[u]>); last first. move/eqP: ot; rewrite eqn_dvd order_dvdn -order_eq1 U'2 ?our //. by rewrite defUv inE Ut. - have p2u: 2.-elt u by rewrite /p_elt ou pnat_exp. + have p2u: 2.-elt u by rewrite /p_elt ou pnatX. have: t \in 'Ohm_1(<[u]>). by rewrite (OhmE _ p2u) mem_gen // !inE Ut -order_dvdn ot. rewrite (Ohm_p_cycle _ p2u) ou pfactorK // subn1 -/r cycle_traject our !inE. @@ -1338,7 +1338,7 @@ have xy2: (x * y) ^+ 2 = x ^+ r. have oxy: #[x * y] = 4 by rewrite (@orderXprime _ 2 2) ?xy2. have r_gt2: r > 2 by rewrite (ltn_exp2l 1) // -(subnKC n_gt3). have coXr1: coprime #[x] (2 ^ (n - 3)).-1. - rewrite ox coprime_expl // -(@coprime_pexpl (n - 3)) ?coprimenP ?subn_gt0 //. + rewrite ox coprimeXl // -(@coprime_pexpl (n - 3)) ?coprimenP ?subn_gt0 //. by rewrite expn_gt0. have def2r1: (2 * (2 ^ (n - 3)).-1).+1 = r.-1. rewrite -!subn1 mulnBr -expnS [_.+1]subnSK ?(ltn_exp2l 0) //. @@ -1584,11 +1584,11 @@ Lemma odd_not_extremal2 : odd #|G| -> ~~ extremal2 G. Proof. rewrite /extremal2 /extremal_class; case: logn => // n'. case: andP => [[n_gt1 isoG] | _]. - by rewrite (card_isog isoG) card_2dihedral ?odd_exp. + by rewrite (card_isog isoG) card_2dihedral ?oddX. case: andP => [[n_gt2 isoG] | _]. - by rewrite (card_isog isoG) card_quaternion ?odd_exp. + by rewrite (card_isog isoG) card_quaternion ?oddX. case: andP => [[n_gt3 isoG] | _]. - by rewrite (card_isog isoG) card_semidihedral ?odd_exp. + by rewrite (card_isog isoG) card_semidihedral ?oddX. by case: ifP. Qed. @@ -1784,7 +1784,7 @@ have[i def_yp]: exists i, y ^- p = x ^+ i. have p_i: p %| i. apply: contraR notXy; rewrite -prime_coprime // => co_p_j. have genX: generator X (y ^- p). - by rewrite def_yp defX generator_coprime ox coprime_expl. + by rewrite def_yp defX generator_coprime ox coprimeXl. rewrite -scXG (setIidPl _) // centsC ((X :=P: _) genX) cycle_subG groupV. rewrite /= -(defG 0%N) mul1g centY inE -defX (subsetP cXX) ?X_Gp //. by rewrite (subsetP (cycle_abelian y)) ?mem_cycle. @@ -1877,7 +1877,7 @@ have modM1 (M : {group gT}): have n_gt2: n > 2 by apply: leq_trans (leq_addl _ _) n_gt23. have def_n: n = (n - 3).+3 by rewrite -{1}(subnKC n_gt2). have oM: #|M| = (q ^ n)%N by rewrite (card_isog isoM) card_modular_group. - have pM: q.-group M by rewrite /pgroup oM pnat_exp pnat_id. + have pM: q.-group M by rewrite /pgroup oM pnatX pnat_id. have def_q: q = p; last rewrite {q q_pr}def_q in oM pM isoM n_gt23. by apply/eqP; rewrite eq_sym [p == q](pgroupP pM) // -iUM dvdn_indexg. have [[x y] genM modM] := generators_modular_group p_pr n_gt2 isoM. diff --git a/mathcomp/solvable/gseries.v b/mathcomp/solvable/gseries.v index a96295f..73188a6 100644 --- a/mathcomp/solvable/gseries.v +++ b/mathcomp/solvable/gseries.v @@ -132,7 +132,7 @@ have:= sKG; rewrite subEproper => /predU1P[<-|prKG]; first exact: IHm. pose L := [group of f G]. have sHK: H \subset K by case/IHm: Hsn. have sLK: L \subset K by rewrite gen_subG class_support_sub_norm. -rewrite -(subnK (proper_card (sub_proper_trans sLK prKG))) iter_add iterSr. +rewrite -(subnK (proper_card (sub_proper_trans sLK prKG))) iterD iterSr. have defH: H = setIgr L H by rewrite -sub_setIgr ?sub_gen ?sub_class_support. have: normal.-series H (map (setIgr L) s) by rewrite defH path_setIgr. case/IHm=> [|_]; first by rewrite size_map. diff --git a/mathcomp/solvable/hall.v b/mathcomp/solvable/hall.v index 119a9fc..6bd5e0d 100644 --- a/mathcomp/solvable/hall.v +++ b/mathcomp/solvable/hall.v @@ -117,7 +117,7 @@ have [sMG nMG] := andP nsMG; rewrite -defG => sK1G coHK oK1K. have nMsG (L : {set gT}): L \subset G -> L \subset 'N(M). by move/subset_trans->. have [coKM coHMK]: coprime #|M| #|K| /\ coprime #|H / M| #|K|. - by apply/andP; rewrite -coprime_mull card_quotient ?nMsG ?Lagrange. + by apply/andP; rewrite -coprimeMl card_quotient ?nMsG ?Lagrange. have oKM (K' : {group gT}): K' \subset G -> #|K'| = #|K| -> #|K' / M| = #|K|. move=> sK'G oK'. rewrite -quotientMidr -?norm_joinEl ?card_quotient ?nMsG //; last first. @@ -248,7 +248,7 @@ have{pi'Hb'} pi'H': pi^'.-nat #|G : H|. by rewrite -(divnMl (cardG_gt0 M)) !Lagrange. have [pi_p | pi'p] := boolP (p \in pi). exists H => //; apply/and3P; split=> //; rewrite /pgroup. - by rewrite -(Lagrange sMH) -card_quotient // pnat_mul -def_H (pi_pnat pM). + by rewrite -(Lagrange sMH) -card_quotient // pnatM -def_H (pi_pnat pM). have [ltHG | leGH {n IHn leGn transH}] := ltnP #|H| #|G|. case: (IHn _ H (leq_trans ltHG leGn)) => [|H1]; first exact: solvableS solG. case/and3P=> sH1H piH1 pi'H1' transH1. @@ -256,7 +256,7 @@ have [ltHG | leGH {n IHn leGn transH}] := ltnP #|H| #|G|. exists H1 => [|K sKG piK]. apply/and3P; split => //. rewrite -divgS // -(Lagrange sHG) -(Lagrange sH1H) -mulnA. - by rewrite mulKn // pnat_mul pi'H1'. + by rewrite mulKn // pnatM pi'H1'. case: (transH K sKG piK) => x Gx def_K. case: (transH1 (K :^ x^-1)%G) => [||y Hy def_K1]. - by rewrite sub_conjgV. @@ -608,7 +608,7 @@ have{nHAq} nHMA: A \subset 'N(HM). by rewrite -(quotientSGK nMA) ?normsG ?quotient_normG -?defHM //; apply/andP. case/orP: (orbN (p \in pi)) => pi_p. exists HM; split=> //; apply/and3P; split; rewrite /pgroup //. - by rewrite -(Lagrange sMHM) pnat_mul -card_quotient // -defHM (pi_pnat pM). + by rewrite -(Lagrange sMHM) pnatM -card_quotient // -defHM (pi_pnat pM). case: (ltnP #|HM| #|G|) => [ltHG | leGHM {n IHn leGn}]. case: (IHn _ A HM X (leq_trans ltHG leGn)) => // [||H [hallH nHA sXH]]. - exact: coprimeSg coGA. @@ -617,7 +617,7 @@ case: (ltnP #|HM| #|G|) => [ltHG | leGHM {n IHn leGn}]. have sHG: H \subset G by apply: subset_trans sHMG. exists H; split=> //; apply/and3P; split=> //. rewrite -divgS // -(Lagrange sHMG) -(Lagrange sHHM) -mulnA mulKn //. - by rewrite pnat_mul pi'H'. + by rewrite pnatM pi'H'. have{leGHM nHMA sHMG sMHM sXHM pi'HM'} eqHMG: HM = G. by apply/eqP; rewrite -val_eqE eqEcard sHMG. have pi'M: pi^'.-group M by rewrite /pgroup (pi_pnat pM). diff --git a/mathcomp/solvable/maximal.v b/mathcomp/solvable/maximal.v index 3786cff..af0001c 100644 --- a/mathcomp/solvable/maximal.v +++ b/mathcomp/solvable/maximal.v @@ -834,7 +834,7 @@ Lemma card_p3group_extraspecial E : prime p -> #|E| = (p ^ 3)%N -> #|'Z(E)| = p -> extraspecial E. Proof. move=> p_pr oEp3 oZp; have p_gt0 := prime_gt0 p_pr. -have pE: p.-group E by rewrite /pgroup oEp3 pnat_exp pnat_id. +have pE: p.-group E by rewrite /pgroup oEp3 pnatX pnat_id. have pEq: p.-group (E / 'Z(E))%g by rewrite quotient_pgroup. have /andP[sZE nZE] := center_normal E. have oEq: #|E / 'Z(E)|%g = (p ^ 2)%N. @@ -1248,7 +1248,7 @@ have [p2 | odd_p] := even_prime p_pr. suffices <-: restr_perm 'Z(E) @* Aut E = Aut 'Z(E) by apply: Aut_in_isog. apply/eqP; rewrite eqEcard restr_perm_Aut ?center_sub //=. by rewrite card_Aut_cyclic ?prime_cyclic ?oZE // {1}p2 cardG_gt0. -have pE: p.-group E by rewrite /pgroup oE pnat_exp pnat_id. +have pE: p.-group E by rewrite /pgroup oE pnatX pnat_id. have nZE: E \subset 'N('Z(E)) by rewrite normal_norm ?center_normal. have esE: extraspecial E := card_p3group_extraspecial p_pr oE oZE. have [[defPhiE defE'] prZ] := esE. @@ -1303,7 +1303,7 @@ pose f := Morphism fM; have fK: f @* K = K. apply/setP=> u; rewrite morphimEdom. apply/imsetP/idP=> [[v Kv ->] | Ku]; first exact: groupX. exists (u ^+ expg_invn K (val k)); first exact: groupX. - rewrite /f /= expgAC expgK // oK coprime_expl // -unitZpE //. + rewrite /f /= expgAC expgK // oK coprimeXl // -unitZpE //. by case: (k) => /=; rewrite orderE -defZ oZE => j; rewrite natr_Zp. have fMact: {in K & <[x]>, morph_act 'J 'J f (idm <[x]>)}. by move=> u v _ _; rewrite /= conjXg. diff --git a/mathcomp/solvable/pgroup.v b/mathcomp/solvable/pgroup.v index 2ed68f0..c9ce3b0 100644 --- a/mathcomp/solvable/pgroup.v +++ b/mathcomp/solvable/pgroup.v @@ -198,7 +198,7 @@ Lemma pgroupM pi G H : pi.-group (G * H) = pi.-group G && pi.-group H. Proof. have GH_gt0: 0 < #|G :&: H| := cardG_gt0 _. rewrite /pgroup -(mulnK #|_| GH_gt0) -mul_cardG -(LagrangeI G H) -mulnA. -by rewrite mulKn // -(LagrangeI H G) setIC !pnat_mul andbCA; case: (pnat _). +by rewrite mulKn // -(LagrangeI H G) setIC !pnatM andbCA; case: (pnat _). Qed. Lemma pgroupJ pi G x : pi.-group (G :^ x) = pi.-group G. @@ -548,8 +548,7 @@ Proof. move=> pi12; rewrite -{2}(consttC pi2 x) consttM; last exact: commuteX2. rewrite (constt1P _ x.`_pi2^' _) ?mulg1 //. apply: sub_in_pnat (p_elt_constt _ x) => p; rewrite order_constt => pi_p. -apply: contra; apply: pi12. -by rewrite -[#[x]](partnC pi2^') // primes_mul // pi_p. +by apply/contra/pi12; rewrite -[#[x]](partnC pi2^') // primesM // pi_p. Qed. Lemma prod_constt x : \prod_(0 <= p < #[x].+1) x.`_p = x. @@ -693,7 +692,7 @@ case/Cauchy=> //= Hx; rewrite -sub1set -gen_subG -/<[Hx]> /order. case/inv_quotientS=> //= K -> sHK sKG {Hx}. rewrite card_quotient ?(subset_trans sKG) // => iKH; apply/negP=> pi_p. rewrite -iKH -divgS // (maxH K) ?divnn ?cardG_gt0 // in p_pr. -by rewrite /psubgroup sKG /pgroup -(Lagrange sHK) mulnC pnat_mul iKH pi_p. +by rewrite /psubgroup sKG /pgroup -(Lagrange sHK) mulnC pnatM iKH pi_p. Qed. Lemma setI_normal_Hall G H K : @@ -725,7 +724,7 @@ Lemma pmorphim_pgroup pi G : Proof. move=> piker sGD; apply/idP/idP=> [pifG|]; last exact: morphim_pgroup. apply: (@pgroupS _ _ (f @*^-1 (f @* G))); first by rewrite -sub_morphim_pre. -by rewrite /pgroup card_morphpre ?morphimS // pnat_mul; apply/andP. +by rewrite /pgroup card_morphpre ?morphimS // pnatM; apply/andP. Qed. Lemma morphim_p_index pi G H : diff --git a/mathcomp/solvable/sylow.v b/mathcomp/solvable/sylow.v index aed6351..fcbe7e8 100644 --- a/mathcomp/solvable/sylow.v +++ b/mathcomp/solvable/sylow.v @@ -267,7 +267,7 @@ Qed. Lemma card_p2group_abelian P : prime p -> #|P| = (p ^ 2)%N -> abelian P. Proof. -move=> primep oP; have pP: p.-group P by rewrite /pgroup oP pnat_exp pnat_id. +move=> primep oP; have pP: p.-group P by rewrite /pgroup oP pnatX pnat_id. by rewrite (p2group_abelian pP) // oP pfactorK. Qed. diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index 4cf0cef..e8293ae 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -443,14 +443,21 @@ Lemma addmCA : left_commutative add. Proof. exact: mulmCA. Qed. Lemma addmAC : right_commutative add. Proof. exact: mulmAC. Qed. Lemma add0m : left_id idm add. Proof. exact: mul1m. Qed. Lemma addm0 : right_id idm add. Proof. exact: mulm1. Qed. -Lemma mulm_addl : left_distributive mul add. Proof. by case add. Qed. -Lemma mulm_addr : right_distributive mul add. Proof. by case add. Qed. +Lemma mulmDl : left_distributive mul add. Proof. by case add. Qed. +Lemma mulmDr : right_distributive mul add. Proof. by case add. Qed. End Add. Definition simpm := (mulm1, mulm0, mul1m, mul0m, mulmA). End Theory. +Notation "@ 'mulm_addl'" := + (deprecate mulm_addl mulmDl) (at level 10, only parsing) : fun_scope. +Notation "@ 'mulm_addr'" := + (deprecate mulm_addr mulmDr) (at level 10, only parsing) : fun_scope. +Notation mulm_addl := (@mulm_addl _ _ _) (only parsing). +Notation mulm_addr := (@mulm_addr _ _ _) (only parsing). + End Theory. Include Theory. @@ -483,7 +490,7 @@ Canonical addn_addoid := AddLaw mulnDl mulnDr. Canonical maxn_monoid := Law maxnA max0n maxn0. Canonical maxn_comoid := ComLaw maxnC. -Canonical maxn_addoid := AddLaw maxn_mull maxn_mulr. +Canonical maxn_addoid := AddLaw maxnMl maxnMr. Canonical gcdn_monoid := Law gcdnA gcd0n gcdn0. Canonical gcdn_comoid := ComLaw gcdnC. @@ -954,7 +961,7 @@ Lemma big_addn m n a (P : pred nat) F : \big[op/idx]_(m + a <= i < n | P i) F i = \big[op/idx]_(m <= i < n - a | P (i + a)) F (i + a). Proof. -rewrite /index_iota -subnDA addnC iota_addl big_map. +rewrite /index_iota -subnDA addnC iotaDl big_map. by apply: eq_big => ? *; rewrite addnC. Qed. @@ -1277,7 +1284,7 @@ Lemma big_cat_nat n m p (P : pred nat) F : m <= n -> n <= p -> \big[*%M/1]_(m <= i < p | P i) F i = (\big[*%M/1]_(m <= i < n | P i) F i) * (\big[*%M/1]_(n <= i < p | P i) F i). Proof. -move=> le_mn le_np; rewrite -big_cat -{2}(subnKC le_mn) -iota_add subnDA. +move=> le_mn le_np; rewrite -big_cat -{2}(subnKC le_mn) -iotaD subnDA. by rewrite subnKC // leq_sub. Qed. @@ -1315,8 +1322,7 @@ Proof. rewrite -(big_map _ _ (lshift n) _ P F) -(big_map _ _ (@rshift m _) _ P F). rewrite -big_cat; congr bigop; apply: (inj_map val_inj). rewrite map_cat -!map_comp (map_comp (addn m)) /=. -rewrite ![index_enum _]unlock unlock !val_ord_enum. -by rewrite -iota_addl addn0 iota_add. +by rewrite ![index_enum _]unlock unlock !val_ord_enum -iotaDl addn0 iotaD. Qed. Lemma big_flatten I rr (P : pred I) F : @@ -1739,11 +1745,11 @@ Local Notation "x + y" := (plus x y). Lemma big_distrl I r a (P : pred I) F : \big[+%M/0]_(i <- r | P i) F i * a = \big[+%M/0]_(i <- r | P i) (F i * a). -Proof. by rewrite (big_endo ( *%M^~ a)) ?mul0m // => x y; apply: mulm_addl. Qed. +Proof. by rewrite (big_endo ( *%M^~ a)) ?mul0m // => x y; apply: mulmDl. Qed. Lemma big_distrr I r a (P : pred I) F : a * \big[+%M/0]_(i <- r | P i) F i = \big[+%M/0]_(i <- r | P i) (a * F i). -Proof. by rewrite big_endo ?mulm0 // => x y; apply: mulm_addr. Qed. +Proof. by rewrite big_endo ?mulm0 // => x y; apply: mulmDr. Qed. Lemma big_distrlr I J rI rJ (pI : pred I) (pJ : pred J) F G : (\big[+%M/0]_(i <- rI | pI i) F i) * (\big[+%M/0]_(j <- rJ | pJ j) G j) diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v index 17e3ac4..4899ee3 100644 --- a/mathcomp/ssreflect/div.v +++ b/mathcomp/ssreflect/div.v @@ -326,7 +326,7 @@ Proof. by rewrite [in RHS](divn_eq m 2) modn2 muln2 addnC half_bit_double. Qed. Lemma odd_mod m d : odd d = false -> odd (m %% d) = odd m. Proof. -by move=> d_even; rewrite [in RHS](divn_eq m d) oddD odd_mul d_even andbF. +by move=> d_even; rewrite [in RHS](divn_eq m d) oddD oddM d_even andbF. Qed. Lemma modnXm m n a : (a %% n) ^ m = a ^ m %[mod n]. @@ -937,33 +937,33 @@ Qed. Lemma Gauss_gcdl p m n : coprime p n -> gcdn p (m * n) = gcdn p m. Proof. by move=> co_pn; rewrite mulnC Gauss_gcdr. Qed. -Lemma coprime_mulr p m n : coprime p (m * n) = coprime p m && coprime p n. +Lemma coprimeMr p m n : coprime p (m * n) = coprime p m && coprime p n. Proof. case co_pm: (coprime p m) => /=; first by rewrite /coprime Gauss_gcdr. apply/eqP=> co_p_mn; case/eqnP: co_pm; apply gcdn_def => // d dv_dp dv_dm. by rewrite -co_p_mn dvdn_gcd dv_dp dvdn_mulr. Qed. -Lemma coprime_mull p m n : coprime (m * n) p = coprime m p && coprime n p. -Proof. by rewrite -!(coprime_sym p) coprime_mulr. Qed. +Lemma coprimeMl p m n : coprime (m * n) p = coprime m p && coprime n p. +Proof. by rewrite -!(coprime_sym p) coprimeMr. Qed. Lemma coprime_pexpl k m n : 0 < k -> coprime (m ^ k) n = coprime m n. Proof. case: k => // k _; elim: k => [|k IHk]; first by rewrite expn1. -by rewrite expnS coprime_mull -IHk; case coprime. +by rewrite expnS coprimeMl -IHk; case coprime. Qed. Lemma coprime_pexpr k m n : 0 < k -> coprime m (n ^ k) = coprime m n. Proof. by move=> k_gt0; rewrite !(coprime_sym m) coprime_pexpl. Qed. -Lemma coprime_expl k m n : coprime m n -> coprime (m ^ k) n. +Lemma coprimeXl k m n : coprime m n -> coprime (m ^ k) n. Proof. by case: k => [|k] co_pm; rewrite ?coprime1n // coprime_pexpl. Qed. -Lemma coprime_expr k m n : coprime m n -> coprime m (n ^ k). -Proof. by rewrite !(coprime_sym m); apply: coprime_expl. Qed. +Lemma coprimeXr k m n : coprime m n -> coprime m (n ^ k). +Proof. by rewrite !(coprime_sym m); apply: coprimeXl. Qed. Lemma coprime_dvdl m n p : m %| n -> coprime n p -> coprime m p. -Proof. by case/dvdnP=> d ->; rewrite coprime_mull => /andP[]. Qed. +Proof. by case/dvdnP=> d ->; rewrite coprimeMl => /andP[]. Qed. Lemma coprime_dvdr m n p : m %| n -> coprime p n -> coprime p m. Proof. by rewrite !(coprime_sym p); apply: coprime_dvdl. Qed. @@ -1040,3 +1040,12 @@ by rewrite chinese_modl chinese_modr !modn_mod !eqxx. Qed. End Chinese. + +Notation "@ 'coprime_expl'" := + (deprecate coprime_expl coprimeXl) (at level 10, only parsing) : fun_scope. +Notation "@ 'coprime_expr'" := + (deprecate coprime_expr coprimeXr) (at level 10, only parsing) : fun_scope. +Notation coprime_mull := (deprecate coprime_mull coprimeMl) (only parsing). +Notation coprime_mulr := (deprecate coprime_mulr coprimeMr) (only parsing). +Notation coprime_expl := (fun k => @coprime_expl k _ _) (only parsing). +Notation coprime_expr := (fun k => @coprime_expr k _ _) (only parsing). diff --git a/mathcomp/ssreflect/fingraph.v b/mathcomp/ssreflect/fingraph.v index b77d1a8..5c933cf 100644 --- a/mathcomp/ssreflect/fingraph.v +++ b/mathcomp/ssreflect/fingraph.v @@ -499,8 +499,8 @@ Lemma iter_finv_in n : {in S, forall x, n <= order x -> iter n finv x = iter (order x - n) f x}. Proof. move=> x xS; rewrite -[x in LHS]iter_order_in => // /subnKC {1}<-. -move: (_ - n) => m; rewrite iter_add; elim: n => // n {2}<-. -by rewrite iterSr /= finv_f_in // -iter_add iter_in. +move: (_ - n) => m; rewrite iterD; elim: n => // n {2}<-. +by rewrite iterSr /= finv_f_in // -iterD iter_in. Qed. Lemma cycle_orbit_in : {in S, forall x, (fcycle f) (orbit x)}. @@ -810,8 +810,8 @@ tfae=> [xorbit_cycle|||[k fkx]|fx y z|/injectivePcycle//]. - apply: (@iter_order_cycle (traject f x k.+1)); rewrite /= ?mem_head//. by apply/fpathP; exists k.+1; rewrite trajectSr -iterSr fkx. - rewrite -!fconnect_orbit => /iter_findex <- /iter_findex <-. - move=> /(congr1 (iter (order x).-1 f)); rewrite -!iterSr !orderSpred. - by rewrite -!iter_add ![order _ + _]addnC !iter_add fx. + move/(congr1 (iter (order x).-1 f)). + by rewrite -!iterSr !orderSpred -!iterD ![order _ + _]addnC !iterD fx. Qed. Lemma order_id_cycle x : fcycle f (orbit x) -> order (f x) = order x. diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v index 4a3eaf1..5b6e4d0 100644 --- a/mathcomp/ssreflect/finset.v +++ b/mathcomp/ssreflect/finset.v @@ -2289,7 +2289,7 @@ Definition fixset := iterF n. Lemma fixsetK : F fixset = fixset. Proof. suff /'exists_eqP[x /= e]: [exists k : 'I_n.+1, iterF k == iterF k.+1]. - by rewrite /fixset -(subnK (leq_ord x)) /iterF iter_add iter_fix. + by rewrite /fixset -(subnK (leq_ord x)) /iterF iterD iter_fix. apply: contraT => /existsPn /(_ (Ordinal _)) /= neq_iter. suff iter_big k : k <= n.+1 -> k <= #|iter k F set0|. by have := iter_big _ (leqnn _); rewrite ltnNge max_card. @@ -2312,7 +2312,7 @@ Proof. by rewrite iter_fix. Qed. Lemma iter_sub_fix k : iterF k \subset fixset. Proof. have [/subset_iter //|/ltnW/subnK<-] := leqP k n; -by rewrite /iterF iter_add fixsetKn. +by rewrite /iterF iterD fixsetKn. Qed. Lemma fix_order_proof x : x \in fixset -> exists n, x \in iterF n. @@ -2396,6 +2396,8 @@ End Greatest. End SetFixpoint. Notation mem_imset := - ((fun aT rT D x f xD => deprecate mem_imset imset_f aT rT f D x xD) _ _ _ _). + ((fun aT rT D x f xD => deprecate mem_imset imset_f aT rT f D x xD) _ _ _ _) + (only parsing). Notation mem_imset2 := ((fun aT aT2 rT D D2 x x2 f xD xD2 => - deprecate mem_imset2 imset2_f aT aT2 rT f D D2 x x2 xD xD2) _ _ _ _ _ _ _). + deprecate mem_imset2 imset2_f aT aT2 rT f D D2 x x2 xD xD2) _ _ _ _ _ _ _) + (only parsing). diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v index 726b8c2..422d760 100644 --- a/mathcomp/ssreflect/fintype.v +++ b/mathcomp/ssreflect/fintype.v @@ -2041,20 +2041,20 @@ Qed. Lemma unbumpK {h} : {in predC1 h, cancel (unbump h) (bump h)}. Proof. by move=> i /negbTE-neq_h_i; rewrite unbumpKcond neq_h_i. Qed. -Lemma bump_addl h i k : bump (k + h) (k + i) = k + bump h i. +Lemma bumpDl h i k : bump (k + h) (k + i) = k + bump h i. Proof. by rewrite /bump leq_add2l addnCA. Qed. Lemma bumpS h i : bump h.+1 i.+1 = (bump h i).+1. Proof. exact: addnS. Qed. -Lemma unbump_addl h i k : unbump (k + h) (k + i) = k + unbump h i. +Lemma unbumpDl h i k : unbump (k + h) (k + i) = k + unbump h i. Proof. apply: (can_inj (bumpK (k + h))). -by rewrite bump_addl !unbumpKcond eqn_add2l addnCA. +by rewrite bumpDl !unbumpKcond eqn_add2l addnCA. Qed. Lemma unbumpS h i : unbump h.+1 i.+1 = (unbump h i).+1. -Proof. exact: unbump_addl 1. Qed. +Proof. exact: unbumpDl 1. Qed. Lemma leq_bump h i j : (i <= bump h j) = (unbump h i <= j). Proof. @@ -2238,7 +2238,7 @@ Proof. by rewrite /inord /insubd valK. Qed. Lemma enum_ordS : enum 'I_n = ord0 :: map (lift ord0) (enum 'I_n'). Proof. apply: (inj_map val_inj); rewrite val_enum_ord /= -map_comp. -by rewrite (map_comp (addn 1)) val_enum_ord -iota_addl. +by rewrite (map_comp (addn 1)) val_enum_ord -iotaDl. Qed. Lemma lift_max (i : 'I_n') : lift ord_max i = i :> nat. @@ -2345,3 +2345,6 @@ Lemma card_sum : #|{: T1 + T2}| = #|T1| + #|T2|. Proof. by rewrite !cardT !enumT [in LHS]unlock size_cat !size_map. Qed. End SumFinType. + +Notation bump_addl := (deprecate bump_addl bumpDl) (only parsing). +Notation unbump_addl := (deprecate unbump_addl unbumpDl) (only parsing). diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index 7d1f0e9..0965b14 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -865,7 +865,7 @@ apply: ihss. rewrite (perm_mem perm_s2) mem_iota => /andP [] _ hy'. apply/allP => n; rewrite (perm_mem perm_s1) mem_iota => /andP []. by rewrite -cat_cons size_cat addnC => /(leq_trans hy'). -- rewrite /= perm_ss andbT perm_merge size_merge size_cat iota_add perm_cat //. +- rewrite /= perm_ss andbT perm_merge size_merge size_cat iotaD perm_cat //. by rewrite addnC -size_cat. Qed. @@ -880,7 +880,7 @@ apply: ihss => /=. apply/allP => m'; rewrite (perm_mem perm_s2) mem_iota => /andP [_ hm']. apply/allP => n; rewrite (perm_mem perm_s1) mem_iota -cat_cons size_cat. by rewrite addnC => /andP [] /(leq_trans hm'). -- rewrite perm_ss andbT perm_merge size_merge size_cat iota_add perm_cat //. +- rewrite perm_ss andbT perm_merge size_merge size_cat iotaD perm_cat //. by rewrite addnC -size_cat. Qed. diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v index 2f35e35..8e94ef6 100644 --- a/mathcomp/ssreflect/prime.v +++ b/mathcomp/ssreflect/prime.v @@ -269,8 +269,8 @@ case def_d: d if_d0 => [|d'] => [[//|{def_m ltdp pr_p} def_m pr_p pr_m'] | _]. rewrite -addnA -doubleD addnCA def_a addSnnS def_k1 -(addnC k) -mulnSr. by rewrite -[_.*2.+1]/p mulnDl doubleD addnA -mul2n mulnA mul2n -mulSn. have next_pm: lb_dvd p.+2 m. - rewrite /lb_dvd /index_iota 2!subSS subn0 -(subnK lt1p) iota_add. - rewrite has_cat; apply/norP; split=> //=; rewrite orbF subnKC // orbC. + rewrite /lb_dvd /index_iota (addKn 2) -(subnK lt1p) iotaD has_cat. + apply/norP; split; rewrite //= orbF subnKC // orbC. apply/norP; split; apply/dvdnP=> [[q def_q]]. case/hasP: leppm; exists 2; first by rewrite /p -(subnKC lt0k). by rewrite /= def_q dvdn_mull // dvdn2 /= odd_double. @@ -549,18 +549,18 @@ Arguments primePns {n}. Lemma pdivP n : n > 1 -> {p | prime p & p %| n}. Proof. by move=> lt1n; exists (pdiv n); rewrite ?pdiv_dvd ?pdiv_prime. Qed. -Lemma primes_mul m n p : m > 0 -> n > 0 -> +Lemma primesM m n p : m > 0 -> n > 0 -> (p \in primes (m * n)) = (p \in primes m) || (p \in primes n). Proof. move=> m_gt0 n_gt0; rewrite !mem_primes muln_gt0 m_gt0 n_gt0. by case pr_p: (prime p); rewrite // Euclid_dvdM. Qed. -Lemma primes_exp m n : n > 0 -> primes (m ^ n) = primes m. +Lemma primesX m n : n > 0 -> primes (m ^ n) = primes m. Proof. case: n => // n _; rewrite expnS; have [-> // | m_gt0] := posnP m. apply/eq_primes => /= p; elim: n => [|n IHn]; first by rewrite muln1. -by rewrite primes_mul ?(expn_gt0, expnS, IHn, orbb, m_gt0). +by rewrite primesM ?(expn_gt0, expnS, IHn, orbb, m_gt0). Qed. Lemma primes_prime p : prime p -> primes p = [::p]. @@ -588,7 +588,7 @@ Lemma pdiv_id p : prime p -> pdiv p = p. Proof. by move=> p_pr; rewrite /pdiv primes_prime. Qed. Lemma pdiv_pfactor p k : prime p -> pdiv (p ^ k.+1) = p. -Proof. by move=> p_pr; rewrite /pdiv primes_exp ?primes_prime. Qed. +Proof. by move=> p_pr; rewrite /pdiv primesX ?primes_prime. Qed. (* Primes are unbounded. *) @@ -707,7 +707,7 @@ have [m0 | m_gt0] := posnP m; first by rewrite m0 prime_coprime ?dvdn0 in co_pm. have mn_gt0: m * n > 0 by rewrite muln_gt0 m_gt0. apply/eqP; rewrite eqn_leq andbC dvdn_leq_log ?dvdn_mull //. set k := logn p _; have: p ^ k %| m * n by rewrite pfactor_dvdn. -by rewrite Gauss_dvdr ?coprime_expl // -pfactor_dvdn. +by rewrite Gauss_dvdr ?coprimeXl // -pfactor_dvdn. Qed. Lemma logn_coprime p m : coprime p m -> logn p m = 0. @@ -747,7 +747,7 @@ exists (logn p d); first by rewrite -(pfactorK n p_pr) dvdn_leq_log. have d_gt0: d > 0 by apply: dvdn_gt0 dv_d_pn. case: (pfactor_coprime p_pr d_gt0) => q co_p_q def_d. rewrite [LHS]def_d ((q =P 1) _) ?mul1n // -dvdn1. -suff: q %| p ^ n * 1 by rewrite Gauss_dvdr // coprime_sym coprime_expl. +suff: q %| p ^ n * 1 by rewrite Gauss_dvdr // coprime_sym coprimeXl. by rewrite muln1 (dvdn_trans _ dv_d_pn) // def_d dvdn_mulr. Qed. @@ -762,7 +762,7 @@ case/mem_prime_decomp=> pr_p _ _. rewrite (big_nth f0) big_mkord (bigD1 (Ordinal lt_i_n)) //=. rewrite def_f mulnC logn_Gauss ?pfactorK //. apply big_ind => [|m1 m2 com1 com2| [j ltj] /=]; first exact: coprimen1. - by rewrite coprime_mulr com1. + by rewrite coprimeMr com1. rewrite -val_eqE /= => nji; case def_j: (nth _ _ j) => [q e1] /=. have: (q, e1) \in prime_decomp n.+1 by rewrite -def_j mem_nth. case/mem_prime_decomp=> pr_q e1_gt0 _; rewrite coprime_pexpr //. @@ -1092,17 +1092,17 @@ Proof. exact: eq_pnat (negnK pi). Qed. Lemma pnatI pi rho n : [predI pi & rho].-nat n = pi.-nat n && rho.-nat n. Proof. by rewrite /pnat andbCA all_predI !andbA andbb. Qed. -Lemma pnat_mul pi m n : pi.-nat (m * n) = pi.-nat m && pi.-nat n. +Lemma pnatM pi m n : pi.-nat (m * n) = pi.-nat m && pi.-nat n. Proof. rewrite /pnat muln_gt0 andbCA -andbA andbCA. case: posnP => // n_gt0; case: posnP => //= m_gt0. apply/allP/andP=> [pi_mn | [pi_m pi_n] p]. - by split; apply/allP=> p m_p; apply: pi_mn; rewrite primes_mul // m_p ?orbT. -by rewrite primes_mul // => /orP[]; [apply: (allP pi_m) | apply: (allP pi_n)]. + by split; apply/allP=> p m_p; apply: pi_mn; rewrite primesM // m_p ?orbT. +by rewrite primesM // => /orP[]; [apply: (allP pi_m) | apply: (allP pi_n)]. Qed. -Lemma pnat_exp pi m n : pi.-nat (m ^ n) = pi.-nat m || (n == 0). -Proof. by case: n => [|n]; rewrite orbC // /pnat expn_gt0 orbC primes_exp. Qed. +Lemma pnatX pi m n : pi.-nat (m ^ n) = pi.-nat m || (n == 0). +Proof. by case: n => [|n]; rewrite orbC // /pnat expn_gt0 orbC primesX. Qed. Lemma part_pnat pi n : pi.-nat n`_pi. Proof. @@ -1131,13 +1131,13 @@ exact: dvdn_trans p_dv_m m_dv_n. Qed. Lemma pi_ofM m n : m > 0 -> n > 0 -> \pi(m * n) =i [predU \pi(m) & \pi(n)]. -Proof. by move=> m_gt0 n_gt0 p; apply: primes_mul. Qed. +Proof. by move=> m_gt0 n_gt0 p; apply: primesM. Qed. Lemma pi_of_part pi n : n > 0 -> \pi(n`_pi) =i [predI \pi(n) & pi]. Proof. by move=> n_gt0 p; rewrite /pi_of primes_part mem_filter andbC. Qed. Lemma pi_of_exp p n : n > 0 -> \pi(p ^ n) = \pi(p). -Proof. by move=> n_gt0; rewrite /pi_of primes_exp. Qed. +Proof. by move=> n_gt0; rewrite /pi_of primesX. Qed. Lemma pi_of_prime p : prime p -> \pi(p) =i (p : nat_pred). Proof. by move=> pr_p q; rewrite /pi_of primes_prime // mem_seq1. Qed. @@ -1155,11 +1155,11 @@ Lemma pnatPpi pi n p : pi.-nat n -> p \in \pi(n) -> p \in pi. Proof. by case/andP=> _ /allP; apply. Qed. Lemma pnat_dvd m n pi : m %| n -> pi.-nat n -> pi.-nat m. -Proof. by case/dvdnP=> q ->; rewrite pnat_mul; case/andP. Qed. +Proof. by case/dvdnP=> q ->; rewrite pnatM; case/andP. Qed. Lemma pnat_div m n pi : m %| n -> pi.-nat n -> pi.-nat (n %/ m). Proof. -case/dvdnP=> q ->; rewrite pnat_mul andbC => /andP[]. +case/dvdnP=> q ->; rewrite pnatM andbC => /andP[]. by case: m => // m _; rewrite mulnK. Qed. @@ -1295,7 +1295,7 @@ rewrite mem_merge mem_cat; case dv_d_p: (p %| d). case pdiv_d: (_ \in _). by case/mapP: pdiv_d dv_d_p => d' _ ->; rewrite natTrecE dvdn_mulr. rewrite mem_divs Gauss_dvdr // coprime_sym. -by rewrite coprime_expl ?prime_coprime ?dv_d_p. +by rewrite coprimeXl ?prime_coprime ?dv_d_p. Qed. Lemma sorted_divisors n : sorted leq (divisors n). @@ -1365,7 +1365,7 @@ Lemma totient_pfactor p e : prime p -> e > 0 -> totient (p ^ e) = p.-1 * p ^ e.-1. Proof. move=> p_pr e_gt0; rewrite totientE ?expn_gt0 ?prime_gt0 //. -by rewrite primes_exp // primes_prime // unlock /= muln1 pfactorK. +by rewrite primesX // primes_prime // unlock /= muln1 pfactorK. Qed. Lemma totient_prime p : prime p -> totient p = p.-1. @@ -1380,13 +1380,13 @@ rewrite !totientE ?muln_gt0 ?m_gt0 //. have /(perm_big _)->: perm_eq (primes (m * n)) (primes m ++ primes n). apply: uniq_perm => [||p]; first exact: primes_uniq. by rewrite cat_uniq !primes_uniq -coprime_has_primes // co_mn. - by rewrite mem_cat primes_mul. + by rewrite mem_cat primesM. rewrite big_cat /= !big_seq. congr (_ * _); apply: eq_bigr => p; rewrite mem_primes => /and3P[_ _ dvp]. rewrite (mulnC m) logn_Gauss //; move: co_mn. - by rewrite -(divnK dvp) coprime_mull => /andP[]. + by rewrite -(divnK dvp) coprimeMl => /andP[]. rewrite logn_Gauss //; move: co_mn. -by rewrite coprime_sym -(divnK dvp) coprime_mull => /andP[]. +by rewrite coprime_sym -(divnK dvp) coprimeMl => /andP[]. Qed. Lemma totient_count_coprime n : totient n = \sum_(0 <= d < n) coprime n d. @@ -1422,9 +1422,17 @@ have ->: totient np = #|[pred d : 'I_np | coprime np d]|. pose h (d : 'I_n) := (in_mod _ np0 d, in_mod _ np'0 d). pose h' (d : 'I_np * 'I_np') := in_mod _ n0 (chinese np np' d.1 d.2). rewrite -!big_mkcond -sum_nat_const pair_big (reindex_onto h h') => [|[d d'] _]. - apply: eq_bigl => [[d ltd] /=]; rewrite !inE /= -val_eqE /= andbC. - rewrite !coprime_modr def_n -chinese_mod // -coprime_mull -def_n. - by rewrite modn_small ?eqxx. + apply: eq_bigl => [[d ltd] /=]; rewrite !inE -val_eqE /= andbC !coprime_modr. + by rewrite def_n -chinese_mod // -coprimeMl -def_n modn_small ?eqxx. apply/eqP; rewrite /eq_op /= /eq_op /= !modn_dvdm ?dvdn_part //. by rewrite chinese_modl // chinese_modr // !modn_small ?eqxx ?ltn_ord. Qed. + +Notation "@ 'primes_mul'" := + (deprecate primes_mul primesM) (at level 10, only parsing) : fun_scope. +Notation "@ 'primes_exp'" := + (deprecate primes_exp primesX) (at level 10, only parsing) : fun_scope. +Notation primes_mul := (@primes_mul _ _) (only parsing). +Notation primes_exp := (fun m => @primes_exp m _) (only parsing). +Notation pnat_mul := (deprecate pnat_mul pnatM) (only parsing). +Notation pnat_exp := (deprecate pnat_exp pnatX) (only parsing). diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 15f9421..7cdc422 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -284,9 +284,8 @@ Lemma cat_cons x s1 s2 : (x :: s1) ++ s2 = x :: s1 ++ s2. Proof. by []. Qed. Lemma cat_nseq n x s : nseq n x ++ s = ncons n x s. Proof. by elim: n => //= n ->. Qed. -Lemma nseqD n1 n2 x : - nseq (n1 + n2) x = nseq n1 x ++ nseq n2 x. -Proof. by rewrite cat_nseq /nseq /ncons iter_add. Qed. +Lemma nseqD n1 n2 x : nseq (n1 + n2) x = nseq n1 x ++ nseq n2 x. +Proof. by rewrite cat_nseq /nseq /ncons iterD. Qed. Lemma cats0 s : s ++ [::] = s. Proof. by elim: s => //= x s ->. Qed. @@ -2504,15 +2503,15 @@ Fixpoint iota m n := if n is n'.+1 then m :: iota m.+1 n' else [::]. Lemma size_iota m n : size (iota m n) = n. Proof. by elim: n m => //= n IHn m; rewrite IHn. Qed. -Lemma iota_add m n1 n2 : iota m (n1 + n2) = iota m n1 ++ iota (m + n1) n2. +Lemma iotaD m n1 n2 : iota m (n1 + n2) = iota m n1 ++ iota (m + n1) n2. Proof. by elim: n1 m => [|n1 IHn1] m; rewrite ?addn0 // -addSnnS /= -IHn1. Qed. -Lemma iota_addl m1 m2 n : iota (m1 + m2) n = map (addn m1) (iota m2 n). +Lemma iotaDl m1 m2 n : iota (m1 + m2) n = map (addn m1) (iota m2 n). Proof. by elim: n m2 => //= n IHn m2; rewrite -addnS IHn. Qed. Lemma nth_iota p m n i : i < n -> nth p (iota m n) i = m + i. Proof. -by move/subnKC <-; rewrite addSnnS iota_add nth_cat size_iota ltnn subnn. +by move/subnKC <-; rewrite addSnnS iotaD nth_cat size_iota ltnn subnn. Qed. Lemma mem_iota m n i : (i \in iota m n) = (m <= i < m + n). @@ -2583,7 +2582,7 @@ elim: t => [|x t IHt] in s It Est *. have /rot_to[k s1 Ds]: x \in s by rewrite (perm_mem Est) mem_head. have [|Is1 eqIst1 Ds1] := IHt s1; first by rewrite -(perm_cons x) -Ds perm_rot. exists (rotr k (0 :: map succn Is1)). - by rewrite perm_rot /It /= perm_cons (iota_addl 1) perm_map. + by rewrite perm_rot /It /= perm_cons (iotaDl 1) perm_map. by rewrite map_rotr /= -map_comp -(@eq_map _ _ (nth x0 t)) // -Ds1 -Ds rotK. Qed. @@ -3581,3 +3580,6 @@ Notation uniq_perm_eq := (deprecate uniq_perm_eq uniq_perm _ _ _) Notation perm_eq_iotaP := (deprecate perm_eq_iotaP perm_iotaP) (only parsing). Notation perm_undup_count := (deprecate perm_undup_count perm_count_undup _ _) (only parsing). + +Notation iota_add := (deprecate iota_add iotaD) (only parsing). +Notation iota_addl := (deprecate iota_addl iotaDl) (only parsing). diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index 8b88821..9f17eb9 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.v @@ -939,7 +939,7 @@ Proof. by elim: n => //= n <-. Qed. Lemma iterS n f x : iter n.+1 f x = f (iter n f x). Proof. by []. Qed. -Lemma iter_add n m f x : iter (n + m) f x = iter n f (iter m f x). +Lemma iterD n m f x : iter (n + m) f x = iter n f (iter m f x). Proof. by elim: n => //= n ->. Qed. Lemma iteriS n f x : iteri n.+1 f x = f n (iteri n f x). @@ -1114,17 +1114,17 @@ move=> lt_mn1 lt_mn2; apply (@leq_ltn_trans (m1 * n2)). by rewrite ltn_pmul2r // (leq_trans _ lt_mn2). Qed. -Lemma maxn_mulr : right_distributive muln maxn. +Lemma maxnMr : right_distributive muln maxn. Proof. by case=> // m n1 n2; rewrite /maxn (fun_if (muln _)) ltn_pmul2l. Qed. -Lemma maxn_mull : left_distributive muln maxn. -Proof. by move=> m1 m2 n; rewrite -!(mulnC n) maxn_mulr. Qed. +Lemma maxnMl : left_distributive muln maxn. +Proof. by move=> m1 m2 n; rewrite -!(mulnC n) maxnMr. Qed. -Lemma minn_mulr : right_distributive muln minn. +Lemma minnMr : right_distributive muln minn. Proof. by case=> // m n1 n2; rewrite /minn (fun_if (muln _)) ltn_pmul2l. Qed. -Lemma minn_mull : left_distributive muln minn. -Proof. by move=> m1 m2 n; rewrite -!(mulnC n) minn_mulr. Qed. +Lemma minnMl : left_distributive muln minn. +Proof. by move=> m1 m2 n; rewrite -!(mulnC n) minnMr. Qed. (* Exponentiation. *) @@ -1276,14 +1276,14 @@ Proof. by move=> le_nm; apply: (@canRL bool) (addbK _) _; rewrite -oddD subnK. Qed. -Lemma odd_opp i m : odd m = false -> i <= m -> odd (m - i) = odd i. -Proof. by move=> oddm le_im; rewrite (oddB (le_im)) oddm. Qed. +Lemma oddN i m : odd m = false -> i <= m -> odd (m - i) = odd i. +Proof. by move=> oddm /oddB ->; rewrite oddm. Qed. -Lemma odd_mul m n : odd (m * n) = odd m && odd n. +Lemma oddM m n : odd (m * n) = odd m && odd n. Proof. by elim: m => //= m IHm; rewrite oddD -addTb andb_addl -IHm. Qed. -Lemma odd_exp m n : odd (m ^ n) = (n == 0) || odd m. -Proof. by elim: n => // n IHn; rewrite expnS odd_mul {}IHn orbC; case odd. Qed. +Lemma oddX m n : odd (m ^ n) = (n == 0) || odd m. +Proof. by elim: n => // n IHn; rewrite expnS oddM {}IHn orbC; case odd. Qed. (* Doubling. *) @@ -1405,7 +1405,7 @@ rewrite -!mulnn mul2n mulnDr !mulnDl (mulnC n) -!addnA. by congr (_ + _); rewrite addnA addnn addnC. Qed. -Lemma sqrn_sub m n : n <= m -> (m - n) ^ 2 = m ^ 2 + n ^ 2 - 2 * (m * n). +Lemma sqrnB m n : n <= m -> (m - n) ^ 2 = m ^ 2 + n ^ 2 - 2 * (m * n). Proof. move/subnK <-; rewrite addnK sqrnD -addnA -addnACA -addnA. by rewrite addnn -mul2n -mulnDr -mulnDl addnK. @@ -1414,7 +1414,7 @@ Qed. Lemma sqrnD_sub m n : n <= m -> (m + n) ^ 2 - 4 * (m * n) = (m - n) ^ 2. Proof. move=> le_nm; rewrite -[4]/(2 * 2) -mulnA mul2n -addnn subnDA. -by rewrite sqrnD addnK sqrn_sub. +by rewrite sqrnD addnK sqrnB. Qed. Lemma subn_sqr m n : m ^ 2 - n ^ 2 = (m - n) * (m + n). @@ -1516,7 +1516,7 @@ Proof. without loss le_nm: m n / n <= m. by have [?|/ltnW ?] := leqP n m; last rewrite eq_sym addnC (mulnC m); apply. apply/leqifP; have [-> | ne_mn] := eqVneq; first by rewrite addnn mul2n. -by rewrite -subn_gt0 -sqrn_sub // sqrn_gt0 subn_gt0 ltn_neqAle eq_sym ne_mn. +by rewrite -subn_gt0 -sqrnB // sqrn_gt0 subn_gt0 ltn_neqAle eq_sym ne_mn. Qed. Lemma nat_AGM2 m n : 4 * (m * n) <= (m + n) ^ 2 ?= iff (m == n). @@ -2035,3 +2035,19 @@ Notation decr_inj := (@decr_inj _) (only parsing). Notation "@ 'decr_inj_in'" := (deprecate decr_inj_in decn_inj_in) (at level 10, only parsing) : fun_scope. Notation decr_inj_in := (@decr_inj_in _ _) (only parsing). + +Notation "@ 'iter_add'" := + (deprecate iter_add iterD) (at level 10, only parsing) : fun_scope. +Notation "@ 'odd_opp'" := + (deprecate odd_opp oddN) (at level 10, only parsing) : fun_scope. +Notation "@ 'sqrn_sub'" := + (deprecate sqrn_sub sqrnB) (at level 10, only parsing) : fun_scope. +Notation iter_add := (@iter_add _) (only parsing). +Notation maxn_mulr := (deprecate maxn_mulr maxnMr) (only parsing). +Notation maxn_mull := (deprecate maxn_mull maxnMl) (only parsing). +Notation minn_mulr := (deprecate minn_mulr minnMr) (only parsing). +Notation minn_mull := (deprecate minn_mull minnMl) (only parsing). +Notation odd_opp := (@odd_opp _ _) (only parsing). +Notation odd_mul := (deprecate odd_mul oddM) (only parsing). +Notation odd_exp := (deprecate odd_exp oddX) (only parsing). +Notation sqrn_sub := (@sqrn_sub _ _) (only parsing). |