diff options
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 3 | ||||
| -rw-r--r-- | mathcomp/algebra/mxpoly.v | 2 | ||||
| -rw-r--r-- | mathcomp/algebra/poly.v | 5 | ||||
| -rw-r--r-- | mathcomp/algebra/polyXY.v | 4 | ||||
| -rw-r--r-- | mathcomp/algebra/polydiv.v | 26 | ||||
| -rw-r--r-- | mathcomp/field/separable.v | 2 |
6 files changed, 16 insertions, 26 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 6fba5bb..83e44b8 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -372,7 +372,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). + `prodrMn` has been renamed `prodrMn_const` (with deprecation alias, cf. Added section) - in `poly.v` - + `polyC_(add|opp|sub|muln|mul|exp|inv)` -> `polyC(D|N|B|Mn|M|X|V)` + + `polyC_(add|opp|sub|muln|mul|inv)` -> `polyC(D|N|B|Mn|M|V)` + `lead_coef_opp` -> `lead_coefN` + `derivn_sub` -> `derivnB` @@ -383,7 +383,6 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). + `dvdp_opp` -> `dvdpNl` + `coprimep_scale(l|r)` -> `coprimepZ(l|r)` + `coprimep_mul(l|r)` -> `coprimepM(l|r)` - + `coprimep_exp(l|r)` -> `coprimepX(l|r)` + `modp_scale(l|r)` -> `modpZ(l|r)` + `modp_(opp|add|scalel|scaler)` -> `modp(N|D|Zl|Zr)` + `divp_(opp|add|scalel|scaler)` -> `divp(N|D|Zl|Zr)` diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v index acf0e95..c7f8fb1 100644 --- a/mathcomp/algebra/mxpoly.v +++ b/mathcomp/algebra/mxpoly.v @@ -938,7 +938,7 @@ Lemma mxdirect_sum_geigenspace {in P &, injective a_} -> mxdirect (\sum_(i | P i) geigenspace g (a_ i)). Proof. move=> /inj_in_eq eq_a; apply: mxdirect_sum_kermx => i j Pi Pj Nji. -by rewrite coprimepXr ?coprimepXl// coprimep_XsubC root_XsubC eq_a. +by rewrite coprimep_expr ?coprimep_expl// coprimep_XsubC root_XsubC eq_a. Qed. Definition eigenpoly n (g : 'M_n) : pred {poly K} := diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v index a95c776..e9e9c45 100644 --- a/mathcomp/algebra/poly.v +++ b/mathcomp/algebra/poly.v @@ -627,7 +627,7 @@ Fact polyC_multiplicative : multiplicative polyC. Proof. by split; first apply: polyCM. Qed. Canonical polyC_rmorphism := AddRMorphism polyC_multiplicative. -Lemma polyCX 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. @@ -2778,8 +2778,6 @@ 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_exp'" := - (deprecate polyC_exp polyCX) (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'" := @@ -2791,7 +2789,6 @@ 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_exp := (@polyC_exp _) (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 5a84da7..fe0acb4 100644 --- a/mathcomp/algebra/polyXY.v +++ b/mathcomp/algebra/polyXY.v @@ -136,7 +136,7 @@ Qed. Lemma max_size_evalC u x : size u.[x%:P] <= sizeY u. Proof. rewrite horner_coef (leq_trans (size_sum _ _ _)) //; apply/bigmax_leqP=> i _. -rewrite (leq_trans (size_mul_leq _ _)) // -polyCX size_polyC addnC -subn1. +rewrite (leq_trans (size_mul_leq _ _)) // -polyC_exp size_polyC addnC -subn1. by rewrite (leq_trans _ (max_size_coefXY _ i)) // leq_subLR leq_add2r leq_b1. Qed. @@ -192,7 +192,7 @@ Lemma horner_swapXY u x : (swapXY u).[x%:P] = u ^ eval x. Proof. apply/polyP=> i /=; rewrite coef_map /= /eval horner_coef coef_sum -sizeYE. rewrite (horner_coef_wide _ (max_size_coefXY u i)); apply: eq_bigr=> j _. -by rewrite -polyCX coefMC coef_swapXY. +by rewrite -polyC_exp coefMC coef_swapXY. Qed. Lemma horner_polyC u x : u.[x%:P] = swapXY u ^ eval x. diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v index 356b8ae..8459c45 100644 --- a/mathcomp/algebra/polydiv.v +++ b/mathcomp/algebra/polydiv.v @@ -427,7 +427,7 @@ move=> lt_rd; case: comm_redivpP=> k q1 r1 /(_ Cdl) Heq. have dn0: d != 0 by case: (size d) lt_rd (size_poly_eq0 d) => // n _ <-. move=> /(_ dn0) Hs. have eC : q * d * (lead_coef d ^+ k)%:P = q * (lead_coef d ^+ k)%:P * d. - by rewrite -mulrA polyCX (commrX k Cdl) mulrA. + by rewrite -mulrA polyC_exp (commrX k Cdl) mulrA. suff e1 : q1 = q * (lead_coef d ^+ k)%:P. congr (_, _, _) => //=; move/eqP: Heq. by rewrite [_ + r1]addrC -subr_eq e1 mulrDl addrAC eC subrr add0r; move/eqP. @@ -463,9 +463,9 @@ suff: (rmodp p d) * (lq ^+ (m - v))%:P == 0. rewrite rreg_div0 //; first by case/andP. by rewrite rreg_size ?ltn_rmodp //; exact: rregX. -rewrite mulrDl addrAC mulNr -!mulrA polyCX -(commrX (m-v) Cdl). -rewrite -polyCX mulrA -mulrDl -rdivp_eq // [(_ ^+ (m - k))%:P]polyCX. -rewrite -(commrX (m-k) Cdl) -polyCX mulrA -he -!mulrA -!polyCM -/v. +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 -!polyCM -/v. by rewrite -!exprD addnC subnK ?leq_maxl // addnC subnK ?subrr ?leq_maxr. Qed. @@ -495,7 +495,7 @@ Proof. have dn0 : d != 0 by rewrite -lead_coef_eq0 rreg_neq0. move: (rdivp_eq d); rewrite rmodpp addr0. suff ->: GRing.comm d (lead_coef d ^+ rscalp d d)%:P by move/(rreg_lead Rreg)->. -by rewrite polyCX; apply: commrX. +by rewrite polyC_exp; apply: commrX. Qed. Lemma rdvdpp : rdvdp d d. Proof. exact/eqP/rmodpp. Qed. @@ -837,8 +837,8 @@ 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 !polyCX -exprMn -polyCM. - by rewrite divrr // expr1n mul1r -polyCX mul_polyC rdivp_eq. + 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. Qed. @@ -2029,11 +2029,11 @@ Qed. Lemma coprimep_pexpr k m n : 0 < k -> coprimep m (n ^+ k) = coprimep m n. Proof. by move=> k_gt0; rewrite !(coprimep_sym m) coprimep_pexpl. Qed. -Lemma coprimepXl k m n : coprimep m n -> coprimep (m ^+ k) n. +Lemma coprimep_expl k m n : coprimep m n -> coprimep (m ^+ k) n. Proof. by case: k => [|k] co_pm; rewrite ?coprime1p // coprimep_pexpl. Qed. -Lemma coprimepXr k m n : coprimep m n -> coprimep m (n ^+ k). -Proof. by rewrite !(coprimep_sym m); apply: coprimepXl. Qed. +Lemma coprimep_expr k m n : coprimep m n -> coprimep m (n ^+ k). +Proof. by rewrite !(coprimep_sym m); apply: coprimep_expl. Qed. Lemma gcdp_mul2l p q r : gcdp (p * q) (p * r) %= (p * gcdp q r). Proof. @@ -2372,10 +2372,6 @@ 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 "@ 'coprimep_expl'" := - (deprecate coprimep_expl coprimepXl) (at level 10, only parsing) : fun_scope. -Notation "@ 'coprimep_expr'" := - (deprecate coprimep_expr coprimepXr) (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). @@ -2383,8 +2379,6 @@ 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). -Notation coprimep_expl := (fun k => @coprimep_expl _ k _ _) (only parsing). -Notation coprimep_expr := (fun k => @coprimep_expr _ k _ _) (only parsing). End CommonIdomain. diff --git a/mathcomp/field/separable.v b/mathcomp/field/separable.v index 0512767..e51a660 100644 --- a/mathcomp/field/separable.v +++ b/mathcomp/field/separable.v @@ -625,7 +625,7 @@ have [K'g]: g \is a polyOver K' /\ q \is a polyOver K'. have /dvdpP[c Dq]: 'X - x%:P %| q by rewrite dvdp_XsubCl root_minPoly. have co_c_g: coprimep c g. have charPp: p \in [char {poly L}] := rmorph_char (polyC_rmorphism _) charLp. - rewrite /g polyCX -!(Frobenius_autE charPp) -rmorphB coprimepXr //. + rewrite /g polyC_exp -!(Frobenius_autE charPp) -rmorphB coprimep_expr //. have: separable_poly q := separable_elementS sKK' sepKx. by rewrite Dq separable_mul => /and3P[]. have{g K'g co_c_g} /size_poly1P[a nz_a Dc]: size c == 1%N. |