diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/algebra/polydiv.v | 4 | ||||
| -rw-r--r-- | mathcomp/algebra/rat.v | 2 | ||||
| -rw-r--r-- | mathcomp/attic/algnum_basic.v | 32 | ||||
| -rw-r--r-- | mathcomp/field/closed_field.v | 12 | ||||
| -rw-r--r-- | mathcomp/odd_order/PFsection7.v | 2 | ||||
| -rw-r--r-- | mathcomp/real_closed/cauchyreals.v | 2 | ||||
| -rw-r--r-- | mathcomp/real_closed/complex.v | 2 | ||||
| -rw-r--r-- | mathcomp/solvable/burnside_app.v | 6 | ||||
| -rw-r--r-- | mathcomp/solvable/gfunctor.v | 2 | ||||
| -rw-r--r-- | mathcomp/solvable/jordanholder.v | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/path.v | 4 |
11 files changed, 35 insertions, 35 deletions
diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v index b6f8936..a3b7ad6 100644 --- a/mathcomp/algebra/polydiv.v +++ b/mathcomp/algebra/polydiv.v @@ -2138,9 +2138,9 @@ Proof. by rewrite mulrC; apply: Gauss_dvdpl. Qed. Lemma Gauss_dvdp m n p : coprimep m n -> (m * n %| p) = (m %| p) && (n %| p). Proof. case: (eqVneq m 0) => [-> | mn0]. - by rewrite coprime0p; move/eqp_dvdl->; rewrite !mul0r dvd0p dvd1p andbT. + by rewrite coprime0p => /eqp_dvdl->; rewrite !mul0r dvd0p dvd1p andbT. case: (eqVneq n 0) => [-> | nn0]. - by rewrite coprimep0; move/eqp_dvdl->; rewrite !mulr0 dvd1p. + by rewrite coprimep0 => /eqp_dvdl->; rewrite !mulr0 dvd1p. move=> hc; apply/idP/idP. move/Gauss_dvdpl: hc => <- h; move/(dvdp_mull m): (h); rewrite dvdp_mul2l //. move->; move/(dvdp_mulr n): (h); rewrite dvdp_mul2r // andbT. diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v index e837ed2..393b37b 100644 --- a/mathcomp/algebra/rat.v +++ b/mathcomp/algebra/rat.v @@ -101,7 +101,7 @@ Proof. by apply: val_inj; rewrite /= gcdn1 !divn1 abszE mulr_sign_norm. Qed. Fact valqK x : fracq (valq x) = x. Proof. move: x => [[n d] /= Pnd]; apply: val_inj=> /=. -move: Pnd; rewrite /coprime /fracq /= => -/andP[] hd -/eqP hnd. +move: Pnd; rewrite /coprime /fracq /= => /andP[] hd -/eqP hnd. by rewrite ltr_gtF ?gtr_eqF //= hnd !divn1 mulz_sign_abs abszE gtr0_norm. Qed. diff --git a/mathcomp/attic/algnum_basic.v b/mathcomp/attic/algnum_basic.v index 54cb1c5..d908b09 100644 --- a/mathcomp/attic/algnum_basic.v +++ b/mathcomp/attic/algnum_basic.v @@ -126,7 +126,7 @@ Qed. Lemma int_clos_incl a : a \in A -> integral a. Proof. move=> ainA; exists ('X - a%:P); rewrite monicXsubC root_XsubC. -rewrite polyOverXsubC => //; by apply Asubr. +rewrite polyOverXsubC => //; by apply: Asubr. Qed. Lemma intPl (I : eqType) G (r : seq I) l : has (fun x => G x != 0) r -> @@ -162,7 +162,7 @@ have rs : size r = n.-1 by rewrite /r size_takel // size_opp leq_pred. exists r; split. apply/eqP => /nilP; rewrite /nilp /r size_takel; last by rewrite size_opp leq_pred. by rewrite -subn1 subn_eq0 leqNgt ps. - have : - p \is a polyOver A by rewrite rpredN //; apply Asubr. + have : - p \is a polyOver A by rewrite rpredN //; apply: Asubr. by move=> /allP-popA; apply/allP => x /mem_take /popA. move: pr => /rootP; rewrite horner_coef -(prednK (n := size p)); last by rewrite ltnW. rewrite big_ord_recr /= rs; have := monicP pm; rewrite /lead_coef => ->; rewrite mul1r => /eqP. @@ -178,7 +178,7 @@ move=> /intPr[ra [/negbTE-ran raA raS]] /intPr[rb [/negbTE-rbn rbA rbS]]. pose n := size ra; pose m := size rb; pose r := Finite.enum [finType of 'I_n * 'I_m]. pose G (z : 'I_n * 'I_m) := let (k, l) := z in a ^ k * b ^l. have [nz mz] : 0 < n /\ 0 < m. - by rewrite !lt0n; split; apply/negP => - /nilP/eqP; rewrite ?ran ?rbn. + by rewrite !lt0n; split; apply/negP => /nilP/eqP; rewrite ?ran ?rbn. have rnn : has (fun x => G x != 0) r. apply/hasP; exists (Ordinal nz, Ordinal mz); first by rewrite /r -enumT mem_enum. by rewrite /G mulr1 oner_neq0. @@ -248,7 +248,7 @@ Hypothesis Aint : int_closed A. Hypothesis Afrac : is_frac_field A 1%AS. Lemma tr_int k l : integral A k -> integral A l -> (tr k l)%:A \in A. -Proof. admit. Qed. +Proof. admit. Admitted. Section NDeg. @@ -367,7 +367,7 @@ Hypothesis Afrac : is_frac_field A K. Hypothesis AsubL : {subset A <= L}. Lemma trK_int k l : integral A k -> integral A l -> ((trK k l)%:A : L0') \in A. -Proof. admit. Qed. +Proof. admit. Admitted. End TraceFieldOver. @@ -429,8 +429,8 @@ suffices FisK (F : fieldType) (L0 : fieldExtType F) (A : pred L0) (L : {subfield have [X Xsize [Xf [Xs Xi]]] := FisK _ L0 _ _ Isubr Iint Ipid Ifrac1 Lnd. rewrite -dim_aspaceOver => //; have /eqP <- := Xsize; exists (in_tuple X); split; last first. split => m; last by move=> /Xi; rewrite /int_closure LK. - by rewrite /int_closure -LK => - /Xs. - move: Xf; rewrite -{1}(in_tupleE X) => - /freeP-XfL0; apply/freeP => k. + by rewrite /int_closure -LK => /Xs. + move: Xf; rewrite -{1}(in_tupleE X) => /freeP-XfL0; apply/freeP => k. have [k' kk'] : exists k' : 'I_(size X) -> F, forall i, (k i)%:A = vsval (k' i). by exists (fun i => vsproj Ifr (k i)%:A) => i; rewrite vsprojK ?rpredZ ?mem1v. pose Ainj := fmorph_inj [rmorphism of in_alg E]. @@ -477,7 +477,7 @@ have Mbasis k (X : k.-tuple L0) M : free X -> module A M -> submod M (span_mod A have seqF (s : seq L0) : all A s -> exists s', s = [seq c%:A | c <- s']. elim: s => [_| a l IHl /= /andP[/Asub1/vlineP[c ->]]]; first by exists [::]. by move=> /IHl[s' ->]; exists (c :: s'). - move=> mM; have := Ms m mM; rewrite /span_mod !size_tuple => - [r rA rS]. + move=> mM; have := Ms m mM; rewrite /span_mod !size_tuple => -[r rA rS]. exists r; split => //; have [rF rFr] := seqF r rA => {seqF}; rewrite rFr in rA. have rFs : size rF = k.+1 by rewrite -(size_tuple r) rFr size_map. have -> : m = \sum_(i < k.+1) rF`_i *: X`_i. @@ -489,13 +489,13 @@ have Mbasis k (X : k.-tuple L0) M : free X -> module A M -> submod M (span_mod A rewrite /module /M1 linear0; split => // a x y aA [xM xfc0] [yM yfc0]. have := Mm a x y aA xM yM; move: aA => /Asub1/vlineP[r] ->; rewrite mulr_algl => msc. by rewrite /M1 linearB linearZ /= xfc0 yfc0 subr0 mulr0. - move=> m [mM mfc0]; have := span_coord m mM => - [r [rA rS rC]]. - move: mfc0 (rC 0) ->; rewrite scale0r => - r0; rewrite /span_mod size_tuple. + move=> m [mM mfc0]; have := span_coord m mM => -[r [rA rS rC]]. + move: mfc0 (rC 0) ->; rewrite scale0r => r0; rewrite /span_mod size_tuple. exists [tuple of behead r]; first by apply/allP => a /mem_behead/(allP rA). by rewrite rS big_ord_recl -r0 mul0r add0r; apply/eq_bigr => i _; rewrite !nth_behead. have [a [w wM wC] aG] : exists2 a, M2 a & forall v, M2 v -> exists2 d, d \in A & d * a = v. apply/Apid; split. - move=> c [m mM <-]; have := span_coord m mM => - [r [/all_nthP-rA _ rC]]. + move=> c [m mM <-]; have := span_coord m mM => -[r [/all_nthP-rA _ rC]]. by move: rC ->; apply/rA; rewrite size_tuple. split; first by exists 0 => //; rewrite linear0 scale0r. move=> c x y cA [mx mxM mxC] [my myM myC]; have := Mm c mx my cA mxM myM. @@ -510,10 +510,10 @@ have Mbasis k (X : k.-tuple L0) M : free X -> module A M -> submod M (span_mod A by rewrite a0 mulr0 scale0r. exists (w :: B1); split. rewrite free_cons B1f andbT; move: an0; apply/contra; move: wC <-. - rewrite -(in_tupleE B1) => - /coord_span ->; apply/eqP. + rewrite -(in_tupleE B1) => /coord_span ->; apply/eqP. rewrite linear_sum big1 ?scale0r => //= i _; rewrite linearZ /=. by have [_] := B1A B1`_i (mem_nth 0 (ltn_ord _)) => ->; rewrite mulr0. - split => [m mM | m]; last by rewrite in_cons => - /orP; case=> [/eqP ->|/B1A[mM]]. + split => [m mM | m]; last by rewrite in_cons => /orP; case=> [/eqP ->|/B1A[mM]]. have [d dA dam] := mcM1 m mM; have mdwM1 : M1 (m - d * w). split; [have Mdwm := Mm d w m dA wM mM; have := Mm _ _ _ A0 Mdwm Mdwm |]. by rewrite mul0r sub0r opprB. @@ -525,16 +525,16 @@ have [X Xb] : exists X, basis_of_mod A (int_closure A L) X. apply/(Mbasis _ b2 _ b2f) => [| m [mL mI]]; first by apply/int_mod_closed. pose r : n.-tuple L0 := [tuple (coord b2 i m)%:A | i < n]; rewrite /span_mod size_tuple. exists r; have rci (i : 'I_n) : r`_i = (coord b2 i m)%:A by rewrite -tnth_nth tnth_mktuple. - apply/(all_nthP 0) => i; rewrite size_tuple => - iB. + apply/(all_nthP 0) => i; rewrite size_tuple => iB. by have -> := rci (Ordinal iB); apply/b2H. - move: mL; rewrite -b2s => - /coord_span ->; apply/eq_bigr => i _. + move: mL; rewrite -b2s => /coord_span ->; apply/eq_bigr => i _. by rewrite rci mulr_algl. exists X => //; move: Xb => [/eqP-Xf [Xs Xg]]; rewrite -Xf eqn_leq; apply/andP; split. by apply/dimvS/span_subvP => m /Xg[mL _]. have /andP[/eqP-b1s _] := b1B; rewrite -b1s; apply/dimvS/span_subvP => b /tnthP-[i ->] {b}. rewrite (tnth_nth 0); have [r /all_tnthP-rA ->] : span_mod A X b1`_i. by apply/Xs; rewrite /int_closure (basis_mem b1B) ?mem_nth ?size_tuple => //. -apply/rpred_sum => j _; have := rA j; rewrite (tnth_nth 0) => - /Asub1/vlineP[c ->]. +apply/rpred_sum => j _; have := rA j; rewrite (tnth_nth 0) => /Asub1/vlineP[c ->]. by rewrite mulr_algl; apply/rpredZ/memv_span/mem_nth. Qed. diff --git a/mathcomp/field/closed_field.v b/mathcomp/field/closed_field.v index 05cf477..5c57df8 100644 --- a/mathcomp/field/closed_field.v +++ b/mathcomp/field/closed_field.v @@ -156,8 +156,8 @@ 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. -by congr (_+_); rewrite addrC. +rewrite Hp mulrDl -!addrA; congr (_ + _); rewrite polyC_add addrC -addrA. +by congr (_ + _); rewrite addrC. Qed. Lemma rsumpT (p q : polyF) : rpoly p -> rpoly q -> rpoly (sumpT p q). @@ -174,7 +174,7 @@ Lemma eval_mulpT (p q : polyF) (e : seq F) : eval_poly e (mulpT p q) = (eval_poly e p) * (eval_poly e q). Proof. elim: p q=> [|a p Hp] q /=; first by rewrite mul0r. -rewrite eval_sumpT /= Hp addr0 mulrDl addrC mulrAC; congr (_+_). +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. Qed. @@ -206,7 +206,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 polyC_muln; congr (_ + _). by rewrite -mulr_natl mulrAC -mulrA mulr_natl mulrC. Qed. @@ -351,7 +351,7 @@ elim: n p q e => /= [| m Pm] p q e. by rewrite redivpTP; last by move=> *; rewrite Pk. rewrite redivpTP; last by move=> *; rewrite !isnullP eval_lift. rewrite isnullP eval_lift; case: (_ == 0); first by rewrite Pk. -by rewrite redivpTP => - *; rewrite ?Pm !eval_lift. +by rewrite redivpTP => *; rewrite ?Pm !eval_lift. Qed. Lemma rgcdp_loopT_qf (p : polyF) (k : polyF -> formula F) (q : polyF) (n : nat) : @@ -629,7 +629,7 @@ constructor; first by apply/holds_conj. by apply/holds_conjn. Qed. -Lemma wf_ex_elim: GRing.wf_QE_proj ex_elim. +Lemma wf_ex_elim : GRing.wf_QE_proj ex_elim. Proof. by move=> i bc /= rbc; apply: ex_elim_qf. Qed. Definition closed_fields_QEMixin := diff --git a/mathcomp/odd_order/PFsection7.v b/mathcomp/odd_order/PFsection7.v index deb1698..559ed7c 100644 --- a/mathcomp/odd_order/PFsection7.v +++ b/mathcomp/odd_order/PFsection7.v @@ -426,7 +426,7 @@ split=> // [ | chi /irrP[t def_chi] o_chiSnu]. have hu: h * u = e^-1 * (h - 1) by rewrite mulrCA (mulrBr h) mulr1 divff. have ->: '[(nu zeta)^\rho] = u * a ^+ 2 - v * a *+ 2 + w. have defT1: perm_eq calT [:: phi, Ind1H, zeta & S2]. - by rewrite defT defS1 (perm_catCA [::_; _] phi). + by rewrite defT defS1 (perm_catCA [:: _; _] phi). have [c ua _ ->] := invDade_seqInd_sum (nu zeta) defT1. have def_c xi: xi \in calS -> c xi = '[xi, zeta]. move=> S2xi; rewrite /c mulrC -{1}[xi]scale1r -(mulVf nz_phi1) -!scalerA. diff --git a/mathcomp/real_closed/cauchyreals.v b/mathcomp/real_closed/cauchyreals.v index 1d7d7ab..1456991 100644 --- a/mathcomp/real_closed/cauchyreals.v +++ b/mathcomp/real_closed/cauchyreals.v @@ -1325,7 +1325,7 @@ have upx_eq0 : u.[x] * p.[x] == 0 by rewrite px0 mul_creal0. pose_big_enough i. have := (erefl ((1 : {poly F}).[x i])). rewrite -{1}hpq /= hornerD hornerC. - set upxi := (u * _).[_] => - hpqi. + set upxi := (u * _).[_] => hpqi. apply: (@neq_crealP ((ubound v.[x])%CR^-1 / 2%:R) i i) => //. by rewrite pmulr_rgt0 ?gtr0E // ubound_gt0. rewrite /= subr0 ler_pdivr_mull ?ubound_gt0 //. diff --git a/mathcomp/real_closed/complex.v b/mathcomp/real_closed/complex.v index 30b4b04..22edf79 100644 --- a/mathcomp/real_closed/complex.v +++ b/mathcomp/real_closed/complex.v @@ -58,7 +58,7 @@ Section ComplexEqChoice. Variable R : Type. -Definition sqR_of_complex (x : R[i]) := let: a +i* b := x in [::a; b]. +Definition sqR_of_complex (x : R[i]) := let: a +i* b := x in [:: a; b]. Definition complex_of_sqR (x : seq R) := if x is [:: a; b] then Some (a +i* b) else None. diff --git a/mathcomp/solvable/burnside_app.v b/mathcomp/solvable/burnside_app.v index d602d0a..d9010d5 100644 --- a/mathcomp/solvable/burnside_app.v +++ b/mathcomp/solvable/burnside_app.v @@ -75,7 +75,7 @@ Ltac inj_tac := move: (erefl rot_inv); unfold rot_inv; match goal with |- ?X = _ -> injective ?Y => move=> _; let x := get_inv Y X in - apply: (can_inj (g:=x)); move => [val H1] + apply: (can_inj (g:=x)); move=> [val H1] end. Lemma R1_inj : injective R1. @@ -1137,10 +1137,10 @@ Qed. Lemma uniq4_uniq6 : forall x y z t : cube, uniq [:: x; y; z; t] -> exists u, exists v, uniq [:: x; y; z; t; u; v]. Proof. -move=> x y z t Uxt; move: ( cardC (mem [:: x; y; z; t])). +move=> x y z t Uxt; move: (cardC (mem [:: x; y; z; t])). rewrite card_ord (card_uniq_tuple Uxt) => hcard. have hcard2: #|predC (mem [:: x; y; z; t])| = 2. - by apply: ( @addnI 4); rewrite /injective hcard. + by apply: (@addnI 4); rewrite /injective hcard. have: #|predC (mem [:: x; y; z; t])| != 0 by rewrite hcard2. case/existsP=> u Hu; exists u. move: (cardC (mem [:: x; y; z; t; u])); rewrite card_ord => hcard5. diff --git a/mathcomp/solvable/gfunctor.v b/mathcomp/solvable/gfunctor.v index 7fbee8c..fc8385d 100644 --- a/mathcomp/solvable/gfunctor.v +++ b/mathcomp/solvable/gfunctor.v @@ -158,7 +158,7 @@ End Definitions. Section ClassDefinitions. Structure iso_map := IsoMap { - apply: object_map; + apply : object_map; _ : group_valued apply; _ : closed apply; _ : iso_continuous apply diff --git a/mathcomp/solvable/jordanholder.v b/mathcomp/solvable/jordanholder.v index 66f6156..7f60bed 100644 --- a/mathcomp/solvable/jordanholder.v +++ b/mathcomp/solvable/jordanholder.v @@ -531,7 +531,7 @@ have: K' :=: 1%G \/ K' :=: (G / H). case; last first. move/quotient_injG; rewrite !inE /=; move/(_ nKH nHG)=> c; move: nsGK. by rewrite c subxx. -rewrite /= -trivg_quotient => - tK'; apply: (congr1 (@gval _)); move: tK'. +rewrite /= -trivg_quotient => tK'; apply: (congr1 (@gval _)); move: tK'. by apply: (@quotient_injG _ H); rewrite ?inE /= ?normal_refl. Qed. diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index 6ab7926..4f3beb4 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -542,9 +542,9 @@ have: perm_eq (catss ss ++ s) (merge_sort_pop s ss). by rewrite perm_catC catA perm_catC perm_cat2l -perm_merge. case: s => // x1 [//|x2 s _]; move/ltnW; move/IHn=> {n IHn}IHs. rewrite -{IHs}(perm_eqrP (IHs _)) ifE; set s1 := if_expr _ _ _. -rewrite (catA _ [::_; _] s) {s}perm_cat2r. +rewrite (catA _ [:: _; _] s) {s}perm_cat2r. apply: (@perm_eq_trans _ (catss ss ++ s1)). - by rewrite perm_cat2l /s1 -ifE; case: ifP; rewrite // (perm_catC [::_]). + by rewrite perm_cat2l /s1 -ifE; case: ifP; rewrite // (perm_catC [:: _]). elim: ss {x1 x2}s1 => /= [|s2 ss IHss] s1; first by rewrite cats0. rewrite perm_catC; case def_s2: {2}s2=> /= [|y s2']; first by rewrite def_s2. by rewrite catA -{IHss}(perm_eqrP (IHss _)) perm_catC perm_cat2l -perm_merge. |