diff options
Diffstat (limited to 'mathcomp/algebra')
| -rw-r--r-- | mathcomp/algebra/matrix.v | 2 | ||||
| -rw-r--r-- | mathcomp/algebra/mxalgebra.v | 59 | ||||
| -rw-r--r-- | mathcomp/algebra/poly.v | 8 | ||||
| -rw-r--r-- | mathcomp/algebra/ssralg.v | 34 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrint.v | 4 | ||||
| -rw-r--r-- | mathcomp/algebra/vector.v | 2 |
6 files changed, 54 insertions, 55 deletions
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index 2501117..3fe8d01 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -2663,7 +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. +Arguments GLval {n%N R ph} u%g. Notation "{ ''GL_' n [ R ] }" := (GLtype n (Phant R)) (at level 0, n at level 2, format "{ ''GL_' n [ R ] }") : type_scope. diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v index af18125..c23d91c 100644 --- a/mathcomp/algebra/mxalgebra.v +++ b/mathcomp/algebra/mxalgebra.v @@ -216,9 +216,9 @@ Definition pinvmx : 'M_(n, m) := End Defs. -Arguments mxrank _%N _%N _%MS. +Arguments mxrank {m%N n%N} A%MS. Local Notation "\rank A" := (mxrank A) : nat_scope. -Arguments complmx _%N _%N _%MS. +Arguments complmx {m%N n%N} A%MS. Local Notation "A ^C" := (complmx A) : matrix_set_scope. Definition submx_def := idfun (fun m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) => @@ -227,21 +227,21 @@ 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. +Arguments submx {m1%N m2%N n%N} A%MS B%MS : rename. 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. +Arguments ltmx {m1%N m2%N n%N} A%MS B%MS. Local Notation "A < B" := (ltmx A B) : matrix_set_scope. Definition eqmx m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) := prod (\rank A = \rank B) (forall m3 (C : 'M_(m3, n)), ((A <= C) = (B <= C)) * ((C <= A) = (C <= B)))%MS. -Arguments eqmx _%N _%N _%N _%MS _%MS. +Arguments eqmx {m1%N m2%N n%N} A%MS B%MS. Local Notation "A :=: B" := (eqmx A B) : matrix_set_scope. Section LtmxIdentities. @@ -296,7 +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. +Arguments addsmx {m1%N m2%N n%N} A%MS B%MS : rename. 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. @@ -330,8 +330,7 @@ Definition capmx_def := idfun (fun m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) => Fact capmx_key : unit. Proof. by []. Qed. Definition capmx := locked_with capmx_key capmx_def. Canonical capmx_unlockable := [unlockable fun capmx]. -Arguments capmx _%N _%N _%N _%MS _%MS. -Prenex Implicits capmx. +Arguments capmx {m1%N m2%N n%N} A%MS B%MS : rename. Local Notation "A :&: B" := (capmx A B) : matrix_set_scope. Local Notation "\bigcap_ ( i | P ) B" := (\big[capmx/1%:M]_(i | P) B) : matrix_set_scope. @@ -341,7 +340,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. +Arguments diffmx {m1%N m2%N n%N} A%MS B%MS : rename. 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. @@ -1725,7 +1724,7 @@ Inductive mxsum_spec n : forall m, 'M[F]_(m, n) -> nat -> Prop := | ProperMxsum m1 m2 T1 T2 r1 r2 of @mxsum_spec n m1 T1 r1 & @mxsum_spec n m2 T2 r2 : mxsum_spec (T1 + T2)%MS (r1 + r2)%N. -Arguments mxsum_spec _%N _%N _%MS _%N. +Arguments mxsum_spec {n%N m%N} T%MS r%N. Structure mxsum_expr m n := Mxsum { mxsum_val :> wrapped 'M_(m, n); @@ -1995,16 +1994,16 @@ 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 diffmx _ _%N _%N _%N _%MS _%MS. -Prenex Implicits genmx. +Arguments mxrank {F m%N n%N} A%MS. +Arguments complmx {F m%N n%N} A%MS. +Arguments row_full {F m%N n%N} A%MS. +Arguments submx {F m1%N m2%N n%N} A%MS B%MS : rename. +Arguments ltmx {F m1%N m2%N n%N} A%MS B%MS. +Arguments eqmx {F m1%N m2%N n%N} A%MS B%MS. +Arguments addsmx {F m1%N m2%N n%N} A%MS B%MS : rename. +Arguments capmx {F m1%N m2%N n%N} A%MS B%MS : rename. +Arguments diffmx {F m1%N m2%N n%N} A%MS B%MS : rename. +Arguments genmx {F m%N n%N} A%R : rename. Notation "\rank A" := (mxrank A) : nat_scope. Notation "<< A >>" := (genmx A) : matrix_set_scope. Notation "A ^C" := (complmx A) : matrix_set_scope. @@ -2279,7 +2278,7 @@ Qed. Definition mulsmx m1 m2 n (R1 : 'A[F]_(m1, n)) (R2 : 'A_(m2, n)) := (\sum_i <<R1 *m lin_mx (mulmxr (vec_mx (row i R2)))>>)%MS. -Arguments mulsmx _%N _%N _%N _%MS _%MS. +Arguments mulsmx {m1%N m2%N n%N} R1%MS R2%MS. Local Notation "R1 * R2" := (mulsmx R1 R2) : matrix_set_scope. @@ -2589,15 +2588,15 @@ Qed. End MatrixAlgebra. -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. -Arguments mxring_id _ _%N _%N _%R _%MS. -Arguments has_mxring_id _ _%N _%N _%R _%MS : extra scopes. -Arguments mxring _ _%N _%N _%MS. -Arguments cent_mx _ _%N _%N _%MS. -Arguments center_mx _ _%N _%N _%MS. +Arguments mulsmx {F m1%N m2%N n%N} R1%MS R2%MS. +Arguments left_mx_ideal {F m1%N m2%N n%N} R%MS S%MS : rename. +Arguments right_mx_ideal {F m1%N m2%N n%N} R%MS S%MS : rename. +Arguments mx_ideal {F m1%N m2%N n%N} R%MS S%MS : rename. +Arguments mxring_id {F m%N n%N} R%MS e%R. +Arguments has_mxring_id {F m%N n%N} R%MS. +Arguments mxring {F m%N n%N} R%MS. +Arguments cent_mx {F m%N n%N} R%MS. +Arguments center_mx {F m%N n%N} R%MS. Notation "A \in R" := (submx (mxvec A) R) : matrix_set_scope. Notation "R * S" := (mulsmx R S) : matrix_set_scope. diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v index 34174bf..929c313 100644 --- a/mathcomp/algebra/poly.v +++ b/mathcomp/algebra/poly.v @@ -146,9 +146,9 @@ End Polynomial. (* directives take effect. *) Bind Scope ring_scope with poly_of. Bind Scope ring_scope with polynomial. -Arguments polyseq _ _%R. -Arguments poly_inj _ _%R _%R _. -Arguments coefp_head _ _ _%N _%R. +Arguments polyseq {R} p%R. +Arguments poly_inj {R} [p1%R p2%R] : rename. +Arguments coefp_head {R} h i%N p%R. Notation "{ 'poly' T }" := (poly_of (Phant T)). Notation coefp i := (coefp_head tt i). @@ -2430,7 +2430,7 @@ Qed. End MapFieldPoly. -Arguments map_poly_inj {F R} f [x1 x2]. +Arguments map_poly_inj {F R} f [p1 p2] : rename. Section MaxRoots. diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v index 854335d..4008f1a 100644 --- a/mathcomp/algebra/ssralg.v +++ b/mathcomp/algebra/ssralg.v @@ -3727,23 +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}. -Arguments Const {R}. +Arguments Add {R} t1%T t2%T. +Arguments Opp {R} t1%T. +Arguments NatMul {R} t1%T n%N. +Arguments Mul {R} t1%T t2%T. +Arguments Inv {R} t1%T. +Arguments Exp {R} t1%T n%N. +Arguments Equal {R} t1%T t2%T. +Arguments Unit {R} t1%T. +Arguments And {R} f1%T f2%T. +Arguments Or {R} f1%T f2%T. +Arguments Implies {R} f1%T f2%T. +Arguments Not {R} f1%T. +Arguments Exists {R} i%N f1%T. +Arguments Forall {R} i%N f1%T. + +Arguments Bool {R} b. +Arguments Const {R} x. Notation True := (Bool true). Notation False := (Bool false). diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v index d0214dd..614fbc2 100644 --- a/mathcomp/algebra/ssrint.v +++ b/mathcomp/algebra/ssrint.v @@ -369,7 +369,7 @@ Canonical int_countIdomainType := [countIdomainType of int]. Definition absz m := match m with Posz p => p | Negz n => n.+1 end. Notation "m - n" := (@GRing.add int_ZmodType m%N (@GRing.opp int_ZmodType n%N)) : distn_scope. -Arguments absz _%distn_scope. +Arguments absz m%distn_scope. Local Notation "`| m |" := (absz m) : nat_scope. Module intOrdered. @@ -1607,7 +1607,7 @@ Module Export IntDist. Notation "m - n" := (@GRing.add int_ZmodType m%N (@GRing.opp int_ZmodType n%N)) : distn_scope. -Arguments absz _%distn_scope. +Arguments absz m%distn_scope. Notation "`| m |" := (absz m) : nat_scope. Coercion Posz : nat >-> int. diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v index aef9a9f..542f8ad 100644 --- a/mathcomp/algebra/vector.v +++ b/mathcomp/algebra/vector.v @@ -245,7 +245,7 @@ Definition f2mx (f : 'Hom(aT, rT)) := let: Hom A := f in A. Canonical hom_subType := [newType for f2mx]. End Hom. -Arguments mx2vs _ _ _%N _%MS. +Arguments mx2vs {K vT m%N} A%MS. Prenex Implicits v2r r2v v2rK r2vK b2mx vs2mx vs2mxK f2mx. End InternalTheory. |