diff options
Diffstat (limited to 'mathcomp/algebra')
| -rw-r--r-- | mathcomp/algebra/intdiv.v | 4 | ||||
| -rw-r--r-- | mathcomp/algebra/interval.v | 2 | ||||
| -rw-r--r-- | mathcomp/algebra/matrix.v | 47 | ||||
| -rw-r--r-- | mathcomp/algebra/mxalgebra.v | 148 | ||||
| -rw-r--r-- | mathcomp/algebra/mxpoly.v | 4 | ||||
| -rw-r--r-- | mathcomp/algebra/poly.v | 12 | ||||
| -rw-r--r-- | mathcomp/algebra/ssralg.v | 35 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 24 | ||||
| -rw-r--r-- | mathcomp/algebra/vector.v | 52 |
9 files changed, 158 insertions, 170 deletions
diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v index 4c5ad4d..933bfcb 100644 --- a/mathcomp/algebra/intdiv.v +++ b/mathcomp/algebra/intdiv.v @@ -340,14 +340,14 @@ apply: (iffP dvdnP) => [] [q Dm]; last by exists `|q|%N; rewrite Dm abszM. exists ((-1) ^+ (m < 0)%R * q%:Z * (-1) ^+ (d < 0)%R). by rewrite -!mulrA -abszEsign -PoszM -Dm -intEsign. Qed. -Arguments dvdzP [d m]. +Arguments dvdzP {d m}. Lemma dvdz_mod0P d m : reflect (m %% d = 0)%Z (d %| m)%Z. Proof. apply: (iffP dvdzP) => [[q ->] | md0]; first by rewrite modzMl. by rewrite (divz_eq m d) md0 addr0; exists (m %/ d)%Z. Qed. -Arguments dvdz_mod0P [d m]. +Arguments dvdz_mod0P {d m}. Lemma dvdz_eq d m : (d %| m)%Z = ((m %/ d)%Z * d == m). Proof. by rewrite (sameP dvdz_mod0P eqP) subr_eq0 eq_sym. Qed. diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v index 80f1b5d..1ca3414 100644 --- a/mathcomp/algebra/interval.v +++ b/mathcomp/algebra/interval.v @@ -134,7 +134,7 @@ Lemma itv_dec : forall (x : R) (i : interval R), reflect (itv_decompose i x) (x \in i). Proof. by move=> x [[[] a|] [[] b|]]; apply: (iffP andP); case. Qed. -Arguments itv_dec [x i]. +Arguments itv_dec {x i}. Definition lersif (x y : R) b := if b then x < y else x <= y. diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index 2a701a2..2501117 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -911,14 +911,13 @@ End VecMatrix. End MatrixStructural. -Arguments const_mx [R m n]. -Arguments row_mxA [R m n1 n2 n3 A1 A2 A3]. -Arguments col_mxA [R m1 m2 m3 n A1 A2 A3]. +Arguments const_mx {R m n}. +Arguments row_mxA {R m n1 n2 n3 A1 A2 A3}. +Arguments col_mxA {R m1 m2 m3 n A1 A2 A3}. Arguments block_mxA - [R m1 m2 m3 n1 n2 n3 A11 A12 A13 A21 A22 A23 A31 A32 A33]. -Prenex Implicits const_mx castmx trmx lsubmx rsubmx usubmx dsubmx row_mx col_mx. + {R m1 m2 m3 n1 n2 n3 A11 A12 A13 A21 A22 A23 A31 A32 A33}. +Prenex Implicits castmx trmx lsubmx rsubmx usubmx dsubmx row_mx col_mx. Prenex Implicits block_mx ulsubmx ursubmx dlsubmx drsubmx. -Prenex Implicits row_mxA col_mxA block_mxA. Prenex Implicits mxvec vec_mx mxvec_indexP mxvecK vec_mxK. Notation "A ^T" := (trmx A) : ring_scope. @@ -2042,20 +2041,18 @@ Definition adjugate n (A : 'M_n) := \matrix[adjugate_key]_(i, j) cofactor A j i. End MatrixAlgebra. -Arguments delta_mx [R m n]. -Arguments scalar_mx [R n]. -Arguments perm_mx [R n]. -Arguments tperm_mx [R n]. -Arguments pid_mx [R m n]. -Arguments copid_mx [R n]. -Arguments lin_mulmxr [R m n p]. -Prenex Implicits delta_mx diag_mx scalar_mx is_scalar_mx perm_mx tperm_mx. -Prenex Implicits pid_mx copid_mx mulmx lin_mulmxr. -Prenex Implicits mxtrace determinant cofactor adjugate. - -Arguments is_scalar_mxP [R n A]. -Arguments mul_delta_mx [R m n p]. -Prenex Implicits mul_delta_mx. +Arguments delta_mx {R m n}. +Arguments scalar_mx {R n}. +Arguments perm_mx {R n}. +Arguments tperm_mx {R n}. +Arguments pid_mx {R m n}. +Arguments copid_mx {R n}. +Arguments lin_mulmxr {R m n p}. +Prenex Implicits diag_mx is_scalar_mx. +Prenex Implicits mulmx mxtrace determinant cofactor adjugate. + +Arguments is_scalar_mxP {R n A}. +Arguments mul_delta_mx {R m n p}. Notation "a %:M" := (scalar_mx a) : ring_scope. Notation "A *m B" := (mulmx A B) : ring_scope. @@ -2500,9 +2497,8 @@ Proof. by rewrite -det_tr tr_block_mx trmx0 det_ublock !det_tr. Qed. End ComMatrix. -Arguments lin_mul_row [R m n]. -Arguments lin_mulmx [R m n p]. -Prenex Implicits lin_mul_row lin_mulmx. +Arguments lin_mul_row {R m n}. +Arguments lin_mulmx {R m n p}. Canonical matrix_finAlgType (R : finComRingType) n' := [finAlgType R of 'M[R]_n'.+1]. @@ -2667,8 +2663,7 @@ Coercion GLval ph (u : GLtype ph) : 'M[R]_n.-1.+1 := End FinUnitMatrix. Bind Scope group_scope with GLtype. -Arguments GLval _%N _ _ _%g. -Prenex Implicits GLval. +Arguments GLval {_%N _ _} _%g. Notation "{ ''GL_' n [ R ] }" := (GLtype n (Phant R)) (at level 0, n at level 2, format "{ ''GL_' n [ R ] }") : type_scope. @@ -2786,7 +2781,7 @@ Qed. End MatrixDomain. -Arguments det0P [R n A]. +Arguments det0P {R n A}. (* Parametricity at the field level (mx_is_scalar, unit and inverse are only *) (* mapped at this level). *) diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v index ed8e6c0..af18125 100644 --- a/mathcomp/algebra/mxalgebra.v +++ b/mathcomp/algebra/mxalgebra.v @@ -227,16 +227,14 @@ Fact submx_key : unit. Proof. by []. Qed. Definition submx := locked_with submx_key submx_def. Canonical submx_unlockable := [unlockable fun submx]. -Arguments submx _%N _%N _%N _%MS _%MS. -Prenex Implicits submx. +Arguments submx {_%N _%N _%N} _%MS _%MS. Local Notation "A <= B" := (submx A B) : matrix_set_scope. Local Notation "A <= B <= C" := ((A <= B) && (B <= C))%MS : matrix_set_scope. Local Notation "A == B" := (A <= B <= A)%MS : matrix_set_scope. Definition ltmx m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) := (A <= B)%MS && ~~ (B <= A)%MS. -Arguments ltmx _%N _%N _%N _%MS _%MS. -Prenex Implicits ltmx. +Arguments ltmx {_%N _%N _%N} _%MS _%MS. Local Notation "A < B" := (ltmx A B) : matrix_set_scope. Definition eqmx m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) := @@ -298,8 +296,7 @@ Definition addsmx_def := idfun (fun m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) => Fact addsmx_key : unit. Proof. by []. Qed. Definition addsmx := locked_with addsmx_key addsmx_def. Canonical addsmx_unlockable := [unlockable fun addsmx]. -Arguments addsmx _%N _%N _%N _%MS _%MS. -Prenex Implicits addsmx. +Arguments addsmx {_%N _%N _%N} _%MS _%MS. Local Notation "A + B" := (addsmx A B) : matrix_set_scope. Local Notation "\sum_ ( i | P ) B" := (\big[addsmx/0]_(i | P) B%MS) : matrix_set_scope. @@ -344,8 +341,7 @@ Definition diffmx_def := idfun (fun m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) => Fact diffmx_key : unit. Proof. by []. Qed. Definition diffmx := locked_with diffmx_key diffmx_def. Canonical diffmx_unlockable := [unlockable fun diffmx]. -Arguments diffmx _%N _%N _%N _%MS _%MS. -Prenex Implicits diffmx. +Arguments diffmx {_%N _%N _%N} _%MS _%MS. Local Notation "A :\: B" := (diffmx A B) : matrix_set_scope. Definition proj_mx n (U V : 'M_n) : 'M_n := pinvmx (col_mx U V) *m col_mx U 0. @@ -505,7 +501,7 @@ Proof. apply: (iffP idP) => [/mulmxKpV | [D ->]]; first by exists (A *m pinvmx B). by rewrite submxE -mulmxA mulmx_coker mulmx0. Qed. -Arguments submxP [m1 m2 n A B]. +Arguments submxP {m1 m2 n A B}. Lemma submx_refl m n (A : 'M_(m, n)) : (A <= A)%MS. Proof. by rewrite submxE mulmx_coker. Qed. @@ -606,7 +602,7 @@ apply: (iffP idP) => [sAB i|sAB]. rewrite submxE; apply/eqP/row_matrixP=> i; apply/eqP. by rewrite row_mul row0 -submxE. Qed. -Arguments row_subP [m1 m2 n A B]. +Arguments row_subP {m1 m2 n A B}. Lemma rV_subP m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : reflect (forall v : 'rV_n, v <= A -> v <= B)%MS (A <= B)%MS. @@ -614,7 +610,7 @@ Proof. apply: (iffP idP) => [sAB v Av | sAB]; first exact: submx_trans sAB. by apply/row_subP=> i; rewrite sAB ?row_sub. Qed. -Arguments rV_subP [m1 m2 n A B]. +Arguments rV_subP {m1 m2 n A B}. Lemma row_subPn m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : reflect (exists i, ~~ (row i A <= B)%MS) (~~ (A <= B)%MS). @@ -662,7 +658,7 @@ apply: (iffP idP) => [Afull | [B kA]]. by exists (1%:M *m pinvmx A); apply: mulmxKpV (submx_full _ Afull). by rewrite [_ A]eqn_leq rank_leq_col (mulmx1_min_rank B 1%:M) ?mulmx1. Qed. -Arguments row_fullP [m n A]. +Arguments row_fullP {m n A}. Lemma row_full_inj m n p A : row_full A -> injective (@mulmx _ m n p A). Proof. @@ -733,7 +729,7 @@ split=> [|m3 C]; first by apply/eqP; rewrite eqn_leq !mxrankS. split; first by apply/idP/idP; apply: submx_trans. by apply/idP/idP=> sC; apply: submx_trans sC _. Qed. -Arguments eqmxP [m1 m2 n A B]. +Arguments eqmxP {m1 m2 n A B}. Lemma rV_eqP m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : reflect (forall u : 'rV_n, (u <= A) = (u <= B))%MS (A == B)%MS. @@ -854,7 +850,7 @@ Proof. apply: (iffP idP) => eqAB; first exact: eq_genmx (eqmxP _). by rewrite -!(genmxE A) eqAB !genmxE andbb. Qed. -Arguments genmxP [m1 m2 n A B]. +Arguments genmxP {m1 m2 n A B}. Lemma genmx0 m n : <<0 : 'M_(m, n)>>%MS = 0. Proof. by apply/eqP; rewrite -submx0 genmxE sub0mx. Qed. @@ -1060,7 +1056,7 @@ apply: (iffP idP) => [|[u ->]]; last by rewrite addmx_sub_adds ?submxMl. rewrite addsmxE; case/submxP=> u ->; exists (lsubmx u, rsubmx u). by rewrite -mul_row_col hsubmxK. Qed. -Arguments sub_addsmxP [m1 m2 m3 n A B C]. +Arguments sub_addsmxP {m1 m2 m3 n A B C}. Variable I : finType. Implicit Type P : pred I. @@ -1784,7 +1780,7 @@ Notation mxdirect A := (mxdirect_def (Phantom 'M_(_,_) A%MS)). Lemma mxdirectP n (S : proper_mxsum_expr n) : reflect (\rank S = proper_mxsum_rank S) (mxdirect S). Proof. exact: eqnP. Qed. -Arguments mxdirectP [n S]. +Arguments mxdirectP {n S}. Lemma mxdirect_trivial m n A : mxdirect (unwrap (@trivial_mxsum m n A)). Proof. exact: eqxx. Qed. @@ -1966,49 +1962,49 @@ End Eigenspace. End RowSpaceTheory. Hint Resolve submx_refl. -Arguments submxP [F m1 m2 n A B]. +Arguments submxP {F m1 m2 n A B}. Arguments eq_row_sub [F m n v A]. -Arguments row_subP [F m1 m2 n A B]. -Arguments rV_subP [F m1 m2 n A B]. -Arguments row_subPn [F m1 m2 n A B]. -Arguments sub_rVP [F n u v]. -Arguments rV_eqP [F m1 m2 n A B]. -Arguments rowV0Pn [F m n A]. -Arguments rowV0P [F m n A]. -Arguments eqmx0P [F m n A]. -Arguments row_fullP [F m n A]. -Arguments row_freeP [F m n A]. -Arguments eqmxP [F m1 m2 n A B]. -Arguments genmxP [F m1 m2 n A B]. -Arguments addsmx_idPr [F m1 m2 n A B]. -Arguments addsmx_idPl [F m1 m2 n A B]. -Arguments sub_addsmxP [F m1 m2 m3 n A B C]. +Arguments row_subP {F m1 m2 n A B}. +Arguments rV_subP {F m1 m2 n A B}. +Arguments row_subPn {F m1 m2 n A B}. +Arguments sub_rVP {F n u v}. +Arguments rV_eqP {F m1 m2 n A B}. +Arguments rowV0Pn {F m n A}. +Arguments rowV0P {F m n A}. +Arguments eqmx0P {F m n A}. +Arguments row_fullP {F m n A}. +Arguments row_freeP {F m n A}. +Arguments eqmxP {F m1 m2 n A B}. +Arguments genmxP {F m1 m2 n A B}. +Arguments addsmx_idPr {F m1 m2 n A B}. +Arguments addsmx_idPl {F m1 m2 n A B}. +Arguments sub_addsmxP {F m1 m2 m3 n A B C}. Arguments sumsmx_sup [F I] i0 [P m n A B_]. -Arguments sumsmx_subP [F I P m n A_ B]. -Arguments sub_sumsmxP [F I P m n A B_]. -Arguments sub_kermxP [F p m n A B]. -Arguments capmx_idPr [F n m1 m2 A B]. -Arguments capmx_idPl [F n m1 m2 A B]. +Arguments sumsmx_subP {F I P m n A_ B}. +Arguments sub_sumsmxP {F I P m n A B_}. +Arguments sub_kermxP {F p m n A B}. +Arguments capmx_idPr {F n m1 m2 A B}. +Arguments capmx_idPl {F n m1 m2 A B}. Arguments bigcapmx_inf [F I] i0 [P m n A_ B]. -Arguments sub_bigcapmxP [F I P m n A B_]. -Arguments mxrank_injP [F m n] p [A f]. -Arguments mxdirectP [F n S]. -Arguments mxdirect_addsP [F m1 m2 n A B]. -Arguments mxdirect_sumsP [F I P n A_]. -Arguments mxdirect_sumsE [F I P n S_]. -Arguments eigenspaceP [F n g a m W]. -Arguments eigenvalueP [F n g a]. - -Arguments mxrank _ _%N _%N _%MS. -Arguments complmx _ _%N _%N _%MS. +Arguments sub_bigcapmxP {F I P m n A B_}. +Arguments mxrank_injP {F m n} p [A f]. +Arguments mxdirectP {F n S}. +Arguments mxdirect_addsP {F m1 m2 n A B}. +Arguments mxdirect_sumsP {F I P n A_}. +Arguments mxdirect_sumsE {F I P n S_}. +Arguments eigenspaceP {F n g a m W}. +Arguments eigenvalueP {F n g a}. + +Arguments mxrank {_ _%N _%N} _%MS. +Arguments complmx {_ _%N _%N} _%MS. Arguments row_full _ _%N _%N _%MS. -Arguments submx _ _%N _%N _%N _%MS _%MS. -Arguments ltmx _ _%N _%N _%N _%MS _%MS. -Arguments eqmx _ _%N _%N _%N _%MS _%MS. -Arguments addsmx _ _%N _%N _%N _%MS _%MS. -Arguments capmx _ _%N _%N _%N _%MS _%MS. +Arguments submx {_ _%N _%N _%N} _%MS _%MS. +Arguments ltmx {_ _%N _%N _%N} _%MS _%MS. +Arguments eqmx {_ _%N _%N _%N} _%MS _%MS. +Arguments addsmx {_ _%N _%N _%N} _%MS _%MS. +Arguments capmx {_ _%N _%N _%N} _%MS _%MS. Arguments diffmx _ _%N _%N _%N _%MS _%MS. -Prenex Implicits mxrank genmx complmx submx ltmx addsmx capmx. +Prenex Implicits genmx. Notation "\rank A" := (mxrank A) : nat_scope. Notation "<< A >>" := (genmx A) : matrix_set_scope. Notation "A ^C" := (complmx A) : matrix_set_scope. @@ -2229,7 +2225,7 @@ Proof. apply: (iffP idP) => [sR12 A R1_A | sR12]; first exact: submx_trans sR12. by apply/rV_subP=> vA; rewrite -(vec_mxK vA); apply: sR12. Qed. -Arguments memmx_subP [m1 m2 n R1 R2]. +Arguments memmx_subP {m1 m2 n R1 R2}. Lemma memmx_eqP m1 m2 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) : reflect (forall A, (A \in R1) = (A \in R2)) (R1 == R2)%MS. @@ -2237,7 +2233,7 @@ Proof. apply: (iffP eqmxP) => [eqR12 A | eqR12]; first by rewrite eqR12. by apply/eqmxP; apply/rV_eqP=> vA; rewrite -(vec_mxK vA) eqR12. Qed. -Arguments memmx_eqP [m1 m2 n R1 R2]. +Arguments memmx_eqP {m1 m2 n R1 R2}. Lemma memmx_addsP m1 m2 n A (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) : reflect (exists D, [/\ D.1 \in R1, D.2 \in R2 & A = D.1 + D.2]) @@ -2249,7 +2245,7 @@ apply: (iffP sub_addsmxP) => [[u /(canRL mxvecK)->] | [D []]]. case/submxP=> u1 defD1 /submxP[u2 defD2] ->. by exists (u1, u2); rewrite linearD /= defD1 defD2. Qed. -Arguments memmx_addsP [m1 m2 n A R1 R2]. +Arguments memmx_addsP {m1 m2 n A R1 R2}. Lemma memmx_sumsP (I : finType) (P : pred I) n (A : 'M_n) R_ : reflect (exists2 A_, A = \sum_(i | P i) A_ i & forall i, A_ i \in R_ i) @@ -2262,7 +2258,7 @@ apply: (iffP sub_sumsmxP) => [[C defA] | [A_ -> R_A] {A}]. exists (fun i => mxvec (A_ i) *m pinvmx (R_ i)). by rewrite linear_sum; apply: eq_bigr => i _; rewrite mulmxKpV. Qed. -Arguments memmx_sumsP [I P n A R_]. +Arguments memmx_sumsP {I P n A R_}. Lemma has_non_scalar_mxP m n (R : 'A_(m, n)) : (1%:M \in R)%MS -> @@ -2312,7 +2308,7 @@ case/memmx_sumsP=> A_ -> R_A; rewrite linear_sum summx_sub //= => j _. rewrite (submx_trans (R_A _)) // genmxE; apply/row_subP=> i. by rewrite row_mul mul_rV_lin sR12R ?vec_mxK ?row_sub. Qed. -Arguments mulsmx_subP [m1 m2 m n R1 R2 R]. +Arguments mulsmx_subP {m1 m2 m n R1 R2 R}. Lemma mulsmxS m1 m2 m3 m4 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) (R3 : 'A_(m3, n)) (R4 : 'A_(m4, n)) : @@ -2347,7 +2343,7 @@ exists A2_ => [i|]; first by rewrite vec_mxK -(genmxE R2) row_sub. apply: eq_bigr => i _; rewrite -[_ *m _](mx_rV_lin (mulmxr_linear _ _)). by rewrite -mulmxA mulmxKpV ?mxvecK // -(genmxE (_ *m _)) R_A. Qed. -Arguments mulsmxP [m1 m2 n A R1 R2]. +Arguments mulsmxP {m1 m2 n A R1 R2}. Lemma mulsmxA m1 m2 m3 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) (R3 : 'A_(m3, n)) : (R1 * (R2 * R3) = R1 * R2 * R3)%MS. @@ -2437,7 +2433,7 @@ congr (row_mx 0 (row_mx (mxvec _) (mxvec _))); apply/row_matrixP=> i. by rewrite !row_mul !mul_rV_lin1 /= mxvecK ideR vec_mxK ?row_sub. by rewrite !row_mul !mul_rV_lin1 /= mxvecK idRe vec_mxK ?row_sub. Qed. -Arguments mxring_idP [m n R]. +Arguments mxring_idP {m n R}. Section CentMxDef. @@ -2473,7 +2469,7 @@ apply: (iffP sub_kermxP); rewrite mul_vec_lin => cBE. apply: (canLR vec_mxK); apply/row_matrixP=> i. by rewrite row_mul mul_rV_lin /= cBE subrr !linear0. Qed. -Arguments cent_rowP [m n B R]. +Arguments cent_rowP {m n B R}. Lemma cent_mxP m n B (R : 'A_(m, n)) : reflect (forall A, A \in R -> A *m B = B *m A) (B \in 'C(R))%MS. @@ -2484,7 +2480,7 @@ apply: (iffP cent_rowP) => cEB => [A sAE | i A]. by rewrite !linearZ -scalemxAl /= cEB. by rewrite cEB // vec_mxK row_sub. Qed. -Arguments cent_mxP [m n B R]. +Arguments cent_mxP {m n B R}. Lemma scalar_mx_cent m n a (R : 'A_(m, n)) : (a%:M \in 'C(R))%MS. Proof. by apply/cent_mxP=> A _; apply: scalar_mxC. Qed. @@ -2499,7 +2495,7 @@ Proof. rewrite sub_capmx; case R_A: (A \in R); last by right; case. by apply: (iffP cent_mxP) => [cAR | [_ cAR]]. Qed. -Arguments center_mxP [m n A R]. +Arguments center_mxP {m n A R}. Lemma mxring_id_uniq m n (R : 'A_(m, n)) e1 e2 : mxring_id R e1 -> mxring_id R e2 -> e1 = e2. @@ -2593,7 +2589,7 @@ Qed. End MatrixAlgebra. -Arguments mulsmx _ _%N _%N _%N _%MS _%MS. +Arguments mulsmx {_ _%N _%N _%N} _%MS _%MS. Arguments left_mx_ideal _ _%N _%N _%N _%MS _%MS. Arguments right_mx_ideal _ _%N _%N _%N _%MS _%MS. Arguments mx_ideal _ _%N _%N _%N _%MS _%MS. @@ -2603,8 +2599,6 @@ Arguments mxring _ _%N _%N _%MS. Arguments cent_mx _ _%N _%N _%MS. Arguments center_mx _ _%N _%N _%MS. -Prenex Implicits mulsmx. - Notation "A \in R" := (submx (mxvec A) R) : matrix_set_scope. Notation "R * S" := (mulsmx R S) : matrix_set_scope. Notation "''C' ( R )" := (cent_mx R) : matrix_set_scope. @@ -2612,16 +2606,16 @@ Notation "''C_' R ( S )" := (R :&: 'C(S))%MS : matrix_set_scope. Notation "''C_' ( R ) ( S )" := ('C_R(S))%MS (only parsing) : matrix_set_scope. Notation "''Z' ( R )" := (center_mx R) : matrix_set_scope. -Arguments memmx_subP [F m1 m2 n R1 R2]. -Arguments memmx_eqP [F m1 m2 n R1 R2]. -Arguments memmx_addsP [F m1 m2 n] A [R1 R2]. -Arguments memmx_sumsP [F I P n A R_]. -Arguments mulsmx_subP [F m1 m2 m n R1 R2 R]. -Arguments mulsmxP [F m1 m2 n A R1 R2]. -Arguments mxring_idP F [m n R]. -Arguments cent_rowP [F m n B R]. -Arguments cent_mxP [F m n B R]. -Arguments center_mxP [F m n A R]. +Arguments memmx_subP {F m1 m2 n R1 R2}. +Arguments memmx_eqP {F m1 m2 n R1 R2}. +Arguments memmx_addsP {F m1 m2 n} A [R1 R2]. +Arguments memmx_sumsP {F I P n A R_}. +Arguments mulsmx_subP {F m1 m2 m n R1 R2 R}. +Arguments mulsmxP {F m1 m2 n A R1 R2}. +Arguments mxring_idP F {m n R}. +Arguments cent_rowP {F m n B R}. +Arguments cent_mxP {F m n B R}. +Arguments center_mxP {F m n A R}. (* Parametricity for the row-space/F-algebra theory. *) Section MapMatrixSpaces. diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v index 7bcd7ed..fe5de6d 100644 --- a/mathcomp/algebra/mxpoly.v +++ b/mathcomp/algebra/mxpoly.v @@ -116,8 +116,8 @@ Canonical rVpoly_linear := Linear rVpoly_is_linear. End RowPoly. -Arguments poly_rV [R d]. -Prenex Implicits rVpoly poly_rV. +Arguments poly_rV {R d}. +Prenex Implicits rVpoly. Section Resultant. diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v index 040b3a8..34174bf 100644 --- a/mathcomp/algebra/poly.v +++ b/mathcomp/algebra/poly.v @@ -1688,11 +1688,11 @@ Notation "a ^` ()" := (deriv a) : ring_scope. Notation "a ^` ( n )" := (derivn n a) : ring_scope. Notation "a ^`N ( n )" := (nderivn n a) : ring_scope. -Arguments monicP [R p]. -Arguments rootP [R p x]. -Arguments rootPf [R p x]. -Arguments rootPt [R p x]. -Arguments unity_rootP [R n z]. +Arguments monicP {R p}. +Arguments rootP {R p x}. +Arguments rootPf {R p x}. +Arguments rootPt {R p x}. +Arguments unity_rootP {R n z}. Arguments polyOverP {R S0 addS kS p}. Canonical polynomial_countZmodType (R : countRingType) := @@ -2611,7 +2611,7 @@ Open Scope unity_root_scope. Definition unity_rootE := unity_rootE. Definition unity_rootP := @unity_rootP. -Arguments unity_rootP [R n z]. +Arguments unity_rootP {R n z}. Definition prim_order_exists := prim_order_exists. Notation prim_order_gt0 := prim_order_gt0. diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v index 9ccb92f..854335d 100644 --- a/mathcomp/algebra/ssralg.v +++ b/mathcomp/algebra/ssralg.v @@ -3727,24 +3727,23 @@ End TermDef. Bind Scope term_scope with term. Bind Scope term_scope with formula. -Arguments Add _ _%T _%T. -Arguments Opp _ _%T. -Arguments NatMul _ _%T _%N. -Arguments Mul _ _%T _%T. -Arguments Inv _ _%T. -Arguments Exp _ _%T _%N. -Arguments Equal _ _%T _%T. -Arguments Unit _ _%T. -Arguments And _ _%T _%T. -Arguments Or _ _%T _%T. -Arguments Implies _ _%T _%T. -Arguments Not _ _%T. -Arguments Exists _ _%N _%T. -Arguments Forall _ _%N _%T. - -Arguments Bool [R]. -Prenex Implicits Const Add Opp NatMul Mul Exp Bool Unit And Or Implies Not. -Prenex Implicits Exists Forall. +Arguments Add {_} _%T _%T. +Arguments Opp {_} _%T. +Arguments NatMul {_} _%T _%N. +Arguments Mul {_} _%T _%T. +Arguments Inv {_} _%T. +Arguments Exp {_} _%T _%N. +Arguments Equal {_} _%T _%T. +Arguments Unit {_} _%T. +Arguments And {_} _%T _%T. +Arguments Or {_} _%T _%T. +Arguments Implies {_} _%T _%T. +Arguments Not {_} _%T. +Arguments Exists {_} _%N _%T. +Arguments Forall {_} _%N _%T. + +Arguments Bool {R}. +Arguments Const {R}. Notation True := (Bool true). Notation False := (Bool false). diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 8d4d3e7..5c6f098 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -1251,11 +1251,11 @@ Definition normrE x := (normr_id, normr0, normr1, normrN1, normr_ge0, normr_eq0, End NumIntegralDomainTheory. -Arguments ler01 [R]. -Arguments ltr01 [R]. -Arguments normr_idP [R x]. -Arguments normr0P [R x]. -Arguments lerifP [R x y C]. +Arguments ler01 {R}. +Arguments ltr01 {R}. +Arguments normr_idP {R x}. +Arguments normr0P {R x}. +Arguments lerifP {R x y C}. Hint Resolve @ler01 @ltr01 lerr ltrr ltrW ltr_eqF ltr0Sn ler0n normr_ge0. Section NumIntegralDomainMonotonyTheory. @@ -2680,7 +2680,7 @@ Lemma real_ler_normlP x y : Proof. by move=> Rx; rewrite real_ler_norml // ler_oppl; apply: (iffP andP) => [] []. Qed. -Arguments real_ler_normlP [x y]. +Arguments real_ler_normlP {x y}. Lemma real_eqr_norml x y : x \is real -> (`|x| == y) = ((x == y) || (x == -y)) && (0 <= y). @@ -2716,7 +2716,7 @@ Proof. move=> Rx; rewrite real_ltr_norml // ltr_oppl. by apply: (iffP (@andP _ _)); case. Qed. -Arguments real_ltr_normlP [x y]. +Arguments real_ltr_normlP {x y}. Lemma real_ler_normr x y : y \is real -> (x <= `|y|) = (x <= y) || (x <= - y). Proof. @@ -3141,9 +3141,9 @@ Hint Resolve ler_opp2 ltr_opp2 real0 real1 normr_real. Arguments ler_sqr {R} [x y]. Arguments ltr_sqr {R} [x y]. Arguments signr_inj {R} [x1 x2]. -Arguments real_ler_normlP [R x y]. -Arguments real_ltr_normlP [R x y]. -Arguments lerif_refl [R x C]. +Arguments real_ler_normlP {R x y}. +Arguments real_ltr_normlP {R x y}. +Arguments lerif_refl {R x C}. Arguments mono_in_lerif [R A f C]. Arguments nmono_in_lerif [R A f C]. Arguments mono_lerif [R f C]. @@ -3631,7 +3631,7 @@ Proof. exact: real_ler_norml. Qed. Lemma ler_normlP x y : reflect ((- x <= y) * (x <= y)) (`|x| <= y). Proof. exact: real_ler_normlP. Qed. -Arguments ler_normlP [x y]. +Arguments ler_normlP {x y}. Lemma eqr_norml x y : (`|x| == y) = ((x == y) || (x == -y)) && (0 <= y). Proof. exact: real_eqr_norml. Qed. @@ -3646,7 +3646,7 @@ Definition lter_norml := (ler_norml, ltr_norml). Lemma ltr_normlP x y : reflect ((-x < y) * (x < y)) (`|x| < y). Proof. exact: real_ltr_normlP. Qed. -Arguments ltr_normlP [x y]. +Arguments ltr_normlP {x y}. Lemma ler_normr x y : (x <= `|y|) = (x <= y) || (x <= - y). Proof. by rewrite lerNgt ltr_norml negb_and -!lerNgt orbC ler_oppr. Qed. diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v index cda2876..aef9a9f 100644 --- a/mathcomp/algebra/vector.v +++ b/mathcomp/algebra/vector.v @@ -1223,27 +1223,27 @@ End BigSumBasis. End VectorTheory. Hint Resolve subvv. -Arguments subvP [K vT U V]. -Arguments addv_idPl [K vT U V]. -Arguments addv_idPr [K vT U V]. -Arguments memv_addP [K vT w U V ]. +Arguments subvP {K vT U V}. +Arguments addv_idPl {K vT U V}. +Arguments addv_idPr {K vT U V}. +Arguments memv_addP {K vT w U V }. Arguments sumv_sup [K vT I] i0 [P U Vs]. -Arguments memv_sumP [K vT I P Us v]. -Arguments subv_sumP [K vT I P Us V]. -Arguments capv_idPl [K vT U V]. -Arguments capv_idPr [K vT U V]. -Arguments memv_capP [K vT w U V]. +Arguments memv_sumP {K vT I P Us v}. +Arguments subv_sumP {K vT I P Us V}. +Arguments capv_idPl {K vT U V}. +Arguments capv_idPr {K vT U V}. +Arguments memv_capP {K vT w U V}. Arguments bigcapv_inf [K vT I] i0 [P Us V]. -Arguments subv_bigcapP [K vT I P U Vs]. -Arguments directvP [K vT S]. -Arguments directv_addP [K vT U V]. -Arguments directv_add_unique [K vT U V]. -Arguments directv_sumP [K vT I P Us]. -Arguments directv_sumE [K vT I P Ss]. -Arguments directv_sum_independent [K vT I P Us]. -Arguments directv_sum_unique [K vT I P Us]. -Arguments span_subvP [K vT X U]. -Arguments freeP [K vT n X]. +Arguments subv_bigcapP {K vT I P U Vs}. +Arguments directvP {K vT S}. +Arguments directv_addP {K vT U V}. +Arguments directv_add_unique {K vT U V}. +Arguments directv_sumP {K vT I P Us}. +Arguments directv_sumE {K vT I P Ss}. +Arguments directv_sum_independent {K vT I P Us}. +Arguments directv_sum_unique {K vT I P Us}. +Arguments span_subvP {K vT X U}. +Arguments freeP {K vT n X}. Prenex Implicits coord. Notation directv S := (directv_def (Phantom _ S%VS)). @@ -1598,11 +1598,11 @@ Proof. by move/lker0_lfunK=> fK; apply/lfunP=> u; rewrite !lfunE /= fK. Qed. End LinearImage. -Arguments memv_imgP [K aT rT f w U]. -Arguments lfunPn [K aT rT f g]. -Arguments lker0P [K aT rT f]. -Arguments eqlfunP [K aT rT f g v]. -Arguments eqlfun_inP [K aT rT V f g]. +Arguments memv_imgP {K aT rT f w U}. +Arguments lfunPn {K aT rT f g}. +Arguments lker0P {K aT rT f}. +Arguments eqlfunP {K aT rT f g v}. +Arguments eqlfun_inP {K aT rT V f g}. Section FixedSpace. @@ -1632,8 +1632,8 @@ Qed. End FixedSpace. -Arguments fixedSpaceP [K vT f a]. -Arguments fixedSpacesP [K vT f U]. +Arguments fixedSpaceP {K vT f a}. +Arguments fixedSpacesP {K vT f U}. Section LinAut. |