diff options
Diffstat (limited to 'mathcomp/field')
| -rw-r--r-- | mathcomp/field/algebraics_fundamentals.v | 4 | ||||
| -rw-r--r-- | mathcomp/field/finfield.v | 4 | ||||
| -rw-r--r-- | mathcomp/field/galois.v | 4 |
3 files changed, 6 insertions, 6 deletions
diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v index 6a28884..2d576c4 100644 --- a/mathcomp/field/algebraics_fundamentals.v +++ b/mathcomp/field/algebraics_fundamentals.v @@ -240,8 +240,8 @@ without loss{nCq} qx0: q mon_q q_dv_p / root (q ^ FtoL) x. have /dvdp_prod_XsubC[m Dq]: q ^ FtoL %| p_ I by rewrite DpI dvdp_map. pose B := [set j in mask m (enum I)]; have{Dq} Dq: q ^ FtoL = p_ B. apply/eqP; rewrite -eqp_monic ?monic_map ?monic_prod_XsubC //. - congr (_ %= _): Dq; apply: eq_big_perm => //. - by rewrite uniq_perm_eq ?mask_uniq ?enum_uniq // => j; rewrite mem_enum inE. + congr (_ %= _): Dq; apply: perm_big => //. + by rewrite uniq_perm ?mask_uniq ?enum_uniq // => j; rewrite mem_enum inE. rewrite -!(size_map_poly FtoL) Dq -DpI (minI B) // -?Dq ?FpxF //. by apply/subsetP=> j; rewrite inE => /mem_mask; rewrite mem_enum. Qed. diff --git a/mathcomp/field/finfield.v b/mathcomp/field/finfield.v index 00a7bad..cb499b3 100644 --- a/mathcomp/field/finfield.v +++ b/mathcomp/field/finfield.v @@ -651,10 +651,10 @@ have prod_aq m: m %| n -> \prod_(d < n.+1 | d %| m) aq d = (q ^ m - 1)%:R. by rewrite !hornerE hornerXn -natrX natrB ?expn_gt0 ?prime_gt0. rewrite (prod_cyclotomic (dvdn_prim_root z_prim m_dv_n)). have def_divm: perm_eq (divisors m) [seq d <- index_iota 0 n.+1 | d %| m]. - rewrite uniq_perm_eq ?divisors_uniq ?filter_uniq ?iota_uniq // => d. + rewrite uniq_perm ?divisors_uniq ?filter_uniq ?iota_uniq // => d. rewrite -dvdn_divisors ?(dvdn_gt0 n_gt0) // mem_filter mem_iota ltnS /=. by apply/esym/andb_idr=> d_dv_m; rewrite dvdn_leq ?(dvdn_trans d_dv_m). - rewrite (eq_big_perm _ def_divm) big_filter big_mkord horner_prod. + rewrite (perm_big _ def_divm) big_filter big_mkord horner_prod. by apply: eq_bigr => d d_dv_m; rewrite -exprM muln_divA ?divnK. have /rpredBl<-: (aq n %| #|G|%:R)%C. rewrite oG -prod_aq // (bigD1 ord_max) //= dvdC_mulr //. diff --git a/mathcomp/field/galois.v b/mathcomp/field/galois.v index ae54fa1..30bef47 100644 --- a/mathcomp/field/galois.v +++ b/mathcomp/field/galois.v @@ -1329,12 +1329,12 @@ rewrite -fixedKE; apply/polyOverP => i; apply/fixedFieldP=> [|x galEx]. rewrite (polyOverP _) // big_map rpred_prod // => b _. by rewrite polyOverXsubC memv_gal. rewrite -coef_map rmorph_prod; congr (_ : {poly _})`_i. -symmetry; rewrite (eq_big_perm (map x r)) /= ?(big_map x). +symmetry; rewrite (perm_big (map x r)) /= ?(big_map x). by apply: eq_bigr => b _; rewrite rmorphB /= map_polyX map_polyC. have Uxr: uniq (map x r) by rewrite map_inj_uniq //; apply: fmorph_inj. have /uniq_min_size: {subset map x r <= r}. by rewrite -map_comp => _ /codomP[b ->] /=; rewrite -galM // r_xa ?groupM. -by rewrite (size_map x) perm_eq_sym; case=> // _ /uniq_perm_eq->. +by rewrite (size_map x) perm_sym; case=> // _ /uniq_perm->. Qed. Lemma mem_galTrace K E a : galois K E -> a \in E -> galTrace K E a \in K. |