diff options
Diffstat (limited to 'mathcomp/algebra')
| -rw-r--r-- | mathcomp/algebra/intdiv.v | 2 | ||||
| -rw-r--r-- | mathcomp/algebra/matrix.v | 4 | ||||
| -rw-r--r-- | mathcomp/algebra/mxalgebra.v | 12 | ||||
| -rw-r--r-- | mathcomp/algebra/poly.v | 2 | ||||
| -rw-r--r-- | mathcomp/algebra/polydiv.v | 14 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrint.v | 2 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 3 | ||||
| -rw-r--r-- | mathcomp/algebra/vector.v | 6 |
8 files changed, 20 insertions, 25 deletions
diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v index 48e9de8..0a5bfde 100644 --- a/mathcomp/algebra/intdiv.v +++ b/mathcomp/algebra/intdiv.v @@ -969,7 +969,7 @@ without loss{IHa} /forallP/(_ (_, _))/= a_dvM: / [forall k, a %| M k.1 k.2]%Z. by exists i; rewrite mxE. exists R^T; last exists L^T; rewrite ?unitmx_tr //; exists d => //. rewrite -[M]trmxK dM !trmx_mul mulmxA; congr (_ *m _ *m _). - by apply/matrixP=> i1 j1; rewrite !mxE eq_sym; case: eqP => // ->. + by apply/matrixP=> i1 j1; rewrite !mxE; case: eqVneq => // ->. without loss{nz_a a_dvM} a1: M a Da / a = 1. pose M1 := map_mx (divz^~ a) M; case/(_ M1 1)=> // [k|L uL [R uR [d dvD dM]]]. by rewrite !mxE Da divzz nz_a. diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index d3142d6..9d6e2be 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -1392,7 +1392,7 @@ Definition diag_mx n (d : 'rV[R]_n) := \matrix[diag_mx_key]_(i, j) (d 0 i *+ (i == j)). Lemma tr_diag_mx n (d : 'rV_n) : (diag_mx d)^T = diag_mx d. -Proof. by apply/matrixP=> i j; rewrite !mxE eq_sym; case: eqP => // ->. Qed. +Proof. by apply/matrixP=> i j; rewrite !mxE; case: eqVneq => // ->. Qed. Lemma diag_mx_is_linear n : linear (@diag_mx n). Proof. @@ -1744,7 +1744,7 @@ by rewrite eqn_leq andbC leqNgt lshift_subproof. Qed. Lemma tr_pid_mx m n r : (pid_mx r)^T = pid_mx r :> 'M_(n, m). -Proof. by apply/matrixP=> i j; rewrite !mxE eq_sym; case: eqP => // ->. Qed. +Proof. by apply/matrixP=> i j; rewrite !mxE; case: eqVneq => // ->. Qed. Lemma pid_mx_minv m n r : pid_mx (minn m r) = pid_mx r :> 'M_(m, n). Proof. by apply/matrixP=> i j; rewrite !mxE leq_min ltn_ord. Qed. diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v index 078fea3..8d6c03b 100644 --- a/mathcomp/algebra/mxalgebra.v +++ b/mathcomp/algebra/mxalgebra.v @@ -2,7 +2,7 @@ (* Distributed under the terms of CeCILL-B. *) From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice. From mathcomp Require Import fintype finfun bigop finset fingroup perm. -From mathcomp Require Import div prime binomial ssralg finalg zmodp matrix. +From mathcomp Require Import div prime binomial ssralg finalg zmodp matrix. (*****************************************************************************) (* In this file we develop the rank and row space theory of matrices, based *) @@ -683,7 +683,7 @@ Qed. Lemma row_full_unit n (A : 'M_n) : row_full A = (A \in unitmx). Proof. exact: row_free_unit. Qed. - + Lemma mxrank_unit n (A : 'M_n) : A \in unitmx -> \rank A = n. Proof. by rewrite -row_full_unit => /eqnP. Qed. @@ -1488,7 +1488,7 @@ Proof. by rewrite unlock; apply/eqmxP; rewrite !genmxE !capmxE andbb. Qed. Lemma genmx_diff m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : (<<A :\: B>> = A :\: B)%MS. Proof. by rewrite [@diffmx]unlock genmx_id. Qed. - + Lemma diffmxSl m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : (A :\: B <= A)%MS. Proof. by rewrite diffmxE capmxSl. Qed. @@ -2202,7 +2202,7 @@ have p_i_gt0: p ^ _ > 0 by move=> i; rewrite expn_gt0 ltnW. rewrite (card_GL _ (ltn0Sn n.-1)) card_ord Fp_cast // big_add1 /=. pose p'gt0 m := m > 0 /\ logn p m = 0%N. suffices [Pgt0 p'P]: p'gt0 (\prod_(0 <= i < n.-1.+1) (p ^ i.+1 - 1))%N. - by rewrite lognM // p'P pfactorK //; case n. + by rewrite lognM // p'P pfactorK // addn0; case n. apply big_ind => [|m1 m2 [m10 p'm1] [m20]|i _]; rewrite {}/p'gt0 ?logn1 //. by rewrite muln_gt0 m10 lognM ?p'm1. rewrite lognE -if_neg subn_gt0 p_pr /= -{1 2}(exp1n i.+1) ltn_exp2r // p_gt1. @@ -2269,7 +2269,7 @@ by rewrite linear_sum; apply: eq_bigr => i _; rewrite mulmxKpV. Qed. Arguments memmx_sumsP {I P n A R_}. -Lemma has_non_scalar_mxP m n (R : 'A_(m, n)) : +Lemma has_non_scalar_mxP m n (R : 'A_(m, n)) : (1%:M \in R)%MS -> reflect (exists2 A, A \in R & ~~ is_scalar_mx A)%MS (1 < \rank R). Proof. @@ -2765,5 +2765,3 @@ 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. - - diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v index d898774..a3b9211 100644 --- a/mathcomp/algebra/poly.v +++ b/mathcomp/algebra/poly.v @@ -368,7 +368,7 @@ Lemma nil_poly p : nilp p = (p == 0). Proof. exact: size_poly_eq0. Qed. Lemma poly0Vpos p : {p = 0} + {size p > 0}. -Proof. by rewrite lt0n size_poly_eq0; apply: eqVneq. Qed. +Proof. by rewrite lt0n size_poly_eq0; case: eqVneq; [left | right]. Qed. Lemma polySpred p : p != 0 -> size p = (size p).-1.+1. Proof. by rewrite -size_poly_eq0 -lt0n => /prednK. Qed. diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v index 6f9d837..b65742d 100644 --- a/mathcomp/algebra/polydiv.v +++ b/mathcomp/algebra/polydiv.v @@ -2037,8 +2037,7 @@ Lemma egcdp_recP : forall k p q, q != 0 -> size q <= k -> size q <= size p -> [/\ size e.1 <= size q, size e.2 <= size p & gcdp p q %= e.1 * p + e.2 * q]. Proof. elim=> [|k ihk] p q /= qn0; first by rewrite leqn0 size_poly_eq0 (negPf qn0). -move=> sqSn qsp; case: (eqVneq q 0)=> q0; first by rewrite q0 eqxx in qn0. -rewrite (negPf qn0). +move=> sqSn qsp; rewrite (negPf qn0). have sp : size p > 0 by apply: leq_trans qsp; rewrite size_poly_gt0. case: (eqVneq (p %% q) 0) => [r0 | rn0] /=. rewrite r0 /egcdp_rec; case: k ihk sqSn => [|n] ihn sqSn /=. @@ -2239,8 +2238,7 @@ Proof. apply/eqP/idP=> [d0|]; last first. case/or3P; [by move/eqP->; rewrite div0p| by move/eqP->; rewrite divp0|]. by move/divp_small. -case: (eqVneq p 0) => [->|pn0]; first by rewrite eqxx. -case: (eqVneq q 0) => [-> | qn0]; first by rewrite eqxx orbT. +case: eqVneq => // _; case: eqVneq => // qn0. move: (divp_eq p q); rewrite d0 mul0r add0r. move/(f_equal (fun x : {poly R} => size x)). by rewrite size_scale ?lc_expn_scalp_neq0 // => ->; rewrite ltn_modp qn0 !orbT. @@ -3039,8 +3037,8 @@ Proof. move=> eqr; rewrite /gdcop; move: (size p)=> n. elim: n p q r eqr {1 3}p (eqpxx p) => [|n ihn] p q r eqr s esp /=. move: eqr; case: (eqVneq q 0)=> [-> | nq0 eqr] /=. - by rewrite eqp_sym eqp0; move->; rewrite eqxx eqpxx. - suff rn0 : r != 0 by rewrite (negPf nq0) (negPf rn0) eqpxx. + by rewrite eqp_sym eqp0 => ->; rewrite eqpxx. + suff rn0 : r != 0 by rewrite (negPf rn0) eqpxx. by apply: contraTneq eqr => ->; rewrite eqp0. rewrite (eqp_coprimepr _ eqr) (eqp_coprimepl _ esp); case: ifP=> _ //. by apply: ihn => //; apply: eqp_div => //; apply: eqp_gcd. @@ -3051,8 +3049,8 @@ Proof. rewrite /rgdcop /gdcop; move: (size p)=> n. elim: n p q {1 3}p {1 3}q (eqpxx p) (eqpxx q) => [|n ihn] p q s t /= sp tq. move: tq; case: (eqVneq t 0)=> [-> | nt0 etq]. - by rewrite eqp_sym eqp0; move->; rewrite eqxx eqpxx. - suff qn0 : q != 0 by rewrite (negPf nt0) (negPf qn0) eqpxx. + by rewrite eqp_sym eqp0 => ->; rewrite eqpxx. + suff qn0 : q != 0 by rewrite (negPf qn0) eqpxx. by apply: contraTneq etq => ->; rewrite eqp0. rewrite rcoprimep_coprimep (eqp_coprimepl t sp) (eqp_coprimepr p tq). case: ifP=> // _; apply: ihn => //; apply: eqp_trans (eqp_rdiv_div _ _) _. diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v index 1b1eb77..3c4c002 100644 --- a/mathcomp/algebra/ssrint.v +++ b/mathcomp/algebra/ssrint.v @@ -1553,7 +1553,7 @@ Lemma abszN1 : `|-1%R| = 1. Proof. by []. Qed. Lemma absz_id m : `|(`|m|)| = `|m|. Proof. by []. Qed. Lemma abszM m1 m2 : `|(m1 * m2)%R| = `|m1| * `|m2|. -Proof. by case: m1 m2 => [[|m1]|m1] [[|m2]|m2]; rewrite //= mulnS mulnC. Qed. +Proof. by case: m1 m2 => [[|m1]|m1] [[|m2]|m2] //=; rewrite ?mulnS mulnC. Qed. Lemma abszX (n : nat) m : `|m ^+ n| = `|m| ^ n. Proof. by elim: n => // n ihn; rewrite exprS expnS abszM ihn. Qed. diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 97afdfb..12fcecb 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -4384,8 +4384,7 @@ have sz_p: size p = n.+1. pose r := sort argCle r0; have r_arg: sorted argCle r by apply: sort_sorted. have{Dp} Dp: p = \prod_(z <- r) ('X - z%:P). rewrite Dp lead_coefE sz_p coefB coefXn coefC -mulrb -mulrnA mulnb lt0n andNb. - rewrite subr0 eqxx scale1r; apply: eq_big_perm. - by rewrite perm_eq_sym perm_sort. + by rewrite subr0 eqxx scale1r; apply/esym/perm_big; rewrite perm_sort. have mem_rP z: (n > 0)%N -> reflect (z ^+ n = x) (z \in r). move=> n_gt0; rewrite -root_prod_XsubC -Dp rootE !hornerE hornerXn n_gt0. by rewrite subr_eq0; apply: eqP. diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v index e73ca33..87ca0f4 100644 --- a/mathcomp/algebra/vector.v +++ b/mathcomp/algebra/vector.v @@ -1004,7 +1004,7 @@ Proof. by rewrite /free span_seq1 dim_vline; case: (~~ _). Qed. Lemma perm_free X Y : perm_eq X Y -> free X = free Y. Proof. -by move=> eqX; rewrite /free (perm_eq_size eqX) (eq_span (perm_eq_mem eqX)). +by move=> eqXY; rewrite /free (perm_size eqXY) (eq_span (perm_mem eqXY)). Qed. Lemma free_directv X : free X = (0 \notin X) && directv (\sum_(v <- X) <[v]>). @@ -1061,7 +1061,7 @@ Proof. by rewrite cat_free => /and3P[]. Qed. Lemma filter_free p X : free X -> free (filter p X). Proof. -rewrite -(perm_free (etrans (perm_filterC p X _) (perm_eq_refl X))). +rewrite -(perm_free (etrans (perm_filterC p X _) (perm_refl X))). exact: catl_free. Qed. @@ -1170,7 +1170,7 @@ Qed. Lemma perm_basis X Y U : perm_eq X Y -> basis_of U X = basis_of U Y. Proof. move=> eqXY; congr ((_ == _) && _); last exact: perm_free. -by apply/eq_span; apply: perm_eq_mem. +by apply/eq_span; apply: perm_mem. Qed. Lemma vbasisP U : basis_of U (vbasis U). |