diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/algebra/matrix.v | 7 | ||||
| -rw-r--r-- | mathcomp/algebra/mxalgebra.v | 2 | ||||
| -rw-r--r-- | mathcomp/algebra/poly.v | 5 | ||||
| -rw-r--r-- | mathcomp/algebra/ssralg.v | 42 | ||||
| -rw-r--r-- | mathcomp/character/character.v | 6 | ||||
| -rw-r--r-- | mathcomp/character/classfun.v | 9 | ||||
| -rw-r--r-- | mathcomp/solvable/gfunctor.v | 5 |
7 files changed, 44 insertions, 32 deletions
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index 9b27ba7..ca71031 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -2429,8 +2429,8 @@ Variables m n p : nat. Implicit Type A : 'M[R]_(m, n). Implicit Type B : 'M[R]_(n, p). -Definition mulmxr_head t B A := let: tt := t in A *m B. -Local Notation mulmxr := (mulmxr_head tt). +Definition mulmxr B A := mulmx A B. +Arguments mulmxr B A /. Definition lin_mulmxr B := lin_mx (mulmxr B). @@ -2451,6 +2451,7 @@ Canonical lin_mulmxr_additive := Additive lin_mulmxr_is_linear. Canonical lin_mulmxr_linear := Linear lin_mulmxr_is_linear. End Mulmxr. +Arguments mulmxr {_ _ _} B A /. (* The trace. *) Section Trace. @@ -2608,7 +2609,7 @@ Hint Extern 0 (is_true (is_trig_mx (diag_mx _))) => Notation "a %:M" := (scalar_mx a) : ring_scope. Notation "A *m B" := (mulmx A B) : ring_scope. -Notation mulmxr := (mulmxr_head tt). +Arguments mulmxr {_ _ _ _} B A /. Notation "\tr A" := (mxtrace A) : ring_scope. Notation "'\det' A" := (determinant A) : ring_scope. Notation "'\adj' A" := (adjugate A) : ring_scope. diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v index dde8843..d707905 100644 --- a/mathcomp/algebra/mxalgebra.v +++ b/mathcomp/algebra/mxalgebra.v @@ -707,7 +707,7 @@ Qed. (* A variant of row_free_inj that exposes mulmxr, an alias for mulmx^~ *) (* but which is canonically additive *) -Definition row_free_injr m n p A : row_free A -> injective (@mulmxr A) := +Definition row_free_injr m n p A : row_free A -> injective (mulmxr A) := @row_free_inj m n p A. Lemma row_free_unit n (A : 'M_n) : row_free A = (A \in unitmx). diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v index c413171..21e8ada 100644 --- a/mathcomp/algebra/poly.v +++ b/mathcomp/algebra/poly.v @@ -140,7 +140,7 @@ Lemma poly_inj : injective polyseq. Proof. exact: val_inj. Qed. Definition poly_of of phant R := polynomial. Identity Coercion type_poly_of : poly_of >-> polynomial. -Definition coefp_head h i (p : poly_of (Phant R)) := let: tt := h in p`_i. +Definition coefp i (p : poly_of (Phant R)) := p`_i. End Polynomial. @@ -150,9 +150,8 @@ Bind Scope ring_scope with poly_of. Bind Scope ring_scope with polynomial. Arguments polyseq {R} p%R. Arguments poly_inj {R} [p1%R p2%R] : rename. -Arguments coefp_head {R} h i%N p%R. +Arguments coefp {R} i%N / p%R. Notation "{ 'poly' T }" := (poly_of (Phant T)). -Notation coefp i := (coefp_head tt i). Definition poly_countMixin (R : countRingType) := [countMixin of polynomial R by <:]. diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v index fa952bb..d1f3072 100644 --- a/mathcomp/algebra/ssralg.v +++ b/mathcomp/algebra/ssralg.v @@ -1856,22 +1856,22 @@ Include Additive.Exports. (* Allows GRing.additive to resolve conflicts. *) Section LiftedZmod. Variables (U : Type) (V : zmodType). Definition null_fun_head (phV : phant V) of U : V := let: Phant := phV in 0. -Definition add_fun_head t (f g : U -> V) x := let: tt := t in f x + g x. -Definition sub_fun_head t (f g : U -> V) x := let: tt := t in f x - g x. +Definition add_fun (f g : U -> V) x := f x + g x. +Definition sub_fun (f g : U -> V) x := f x - g x. End LiftedZmod. (* Lifted multiplication. *) Section LiftedRing. Variables (R : ringType) (T : Type). Implicit Type f : T -> R. -Definition mull_fun_head t a f x := let: tt := t in a * f x. -Definition mulr_fun_head t a f x := let: tt := t in f x * a. +Definition mull_fun a f x := a * f x. +Definition mulr_fun a f x := f x * a. End LiftedRing. (* Lifted linear operations. *) Section LiftedScale. Variables (R : ringType) (U : Type) (V : lmodType R) (A : lalgType R). -Definition scale_fun_head t a (f : U -> V) x := let: tt := t in a *: f x. +Definition scale_fun a (f : U -> V) x := a *: f x. Definition in_alg_head (phA : phant A) k : A := let: Phant := phA in k%:A. End LiftedScale. @@ -1881,11 +1881,17 @@ Notation null_fun V := (null_fun_head (Phant V)) (only parsing). Local Notation in_alg_loc A := (in_alg_head (Phant A)) (only parsing). Local Notation "\0" := (null_fun _) : ring_scope. -Local Notation "f \+ g" := (add_fun_head tt f g) : ring_scope. -Local Notation "f \- g" := (sub_fun_head tt f g) : ring_scope. -Local Notation "a \*: f" := (scale_fun_head tt a f) : ring_scope. -Local Notation "x \*o f" := (mull_fun_head tt x f) : ring_scope. -Local Notation "x \o* f" := (mulr_fun_head tt x f) : ring_scope. +Local Notation "f \+ g" := (add_fun f g) : ring_scope. +Local Notation "f \- g" := (sub_fun f g) : ring_scope. +Local Notation "a \*: f" := (scale_fun a f) : ring_scope. +Local Notation "x \*o f" := (mull_fun x f) : ring_scope. +Local Notation "x \o* f" := (mulr_fun x f) : ring_scope. + +Arguments add_fun {_ _} f g _ /. +Arguments sub_fun {_ _} f g _ /. +Arguments mull_fun {_ _} a f _ /. +Arguments mulr_fun {_ _} a f _ /. +Arguments scale_fun {_ _ _} a f _ /. Section AdditiveTheory. @@ -6084,11 +6090,17 @@ Notation "*:%R" := (@scale _ _). Notation "a *: m" := (scale a m) : ring_scope. Notation "k %:A" := (scale k 1) : ring_scope. Notation "\0" := (null_fun _) : ring_scope. -Notation "f \+ g" := (add_fun_head tt f g) : ring_scope. -Notation "f \- g" := (sub_fun_head tt f g) : ring_scope. -Notation "a \*: f" := (scale_fun_head tt a f) : ring_scope. -Notation "x \*o f" := (mull_fun_head tt x f) : ring_scope. -Notation "x \o* f" := (mulr_fun_head tt x f) : ring_scope. +Notation "f \+ g" := (add_fun f g) : ring_scope. +Notation "f \- g" := (sub_fun f g) : ring_scope. +Notation "a \*: f" := (scale_fun a f) : ring_scope. +Notation "x \*o f" := (mull_fun x f) : ring_scope. +Notation "x \o* f" := (mulr_fun x f) : ring_scope. + +Arguments add_fun {_ _} f g _ /. +Arguments sub_fun {_ _} f g _ /. +Arguments mull_fun {_ _} a f _ /. +Arguments mulr_fun {_ _} a f _ /. +Arguments scale_fun {_ _ _} a f _ /. Notation "\sum_ ( i <- r | P ) F" := (\big[+%R/0%R]_(i <- r | P%B) F%R) : ring_scope. diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v index 58a3688..31a7aa5 100644 --- a/mathcomp/character/character.v +++ b/mathcomp/character/character.v @@ -508,8 +508,8 @@ Lemma xcfunZr a phi A : xcfun phi (a *: A) = a * xcfun phi A. Proof. by rewrite /xcfun linearZ -scalemxAl mxE. Qed. (* In order to add a second canonical structure on xcfun *) -Definition xcfun_r_head k A phi := let: tt := k in xcfun phi A. -Local Notation xcfun_r A := (xcfun_r_head tt A). +Definition xcfun_r A phi := xcfun phi A. +Arguments xcfun_r A phi /. Lemma xcfun_rE A chi : xcfun_r A chi = xcfun chi A. Proof. by []. Qed. @@ -534,7 +534,7 @@ by congr (_ * \tr _) => {A} /=; rewrite /gring_mx /= -rowE rowK mxvecK. Qed. End Char. -Notation xcfun_r A := (xcfun_r_head tt A). +Arguments xcfun_r {_ _} A phi /. Notation "phi .[ A ]" := (xcfun phi A) : cfun_scope. Definition pred_Nirr gT B := #|@classes gT B|.-1. diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v index 2bea267..17b1490 100644 --- a/mathcomp/character/classfun.v +++ b/mathcomp/character/classfun.v @@ -378,8 +378,8 @@ Definition cfun_base A : #|classes B ::&: A|.-tuple classfun := Definition classfun_on A := <<cfun_base A>>%VS. Definition cfdot phi psi := #|B|%:R^-1 * \sum_(x in B) phi x * (psi x)^*. -Definition cfdotr_head k psi phi := let: tt := k in cfdot phi psi. -Definition cfnorm_head k phi := let: tt := k in cfdot phi phi. +Definition cfdotr psi phi := cfdot phi psi. +Definition cfnorm phi := cfdot phi phi. Coercion seq_of_cfun phi := [:: phi]. @@ -395,7 +395,8 @@ Arguments cfun_indicator {gT} B%g. Arguments cfAut {gT B%g} u phi%CF. Arguments cfReal {gT B%g} phi%CF. Arguments cfdot {gT B%g} phi%CF psi%CF. -Arguments cfdotr_head {gT B%g} k psi%CF phi%CF. +Arguments cfdotr {gT B%g} psi%CF phi%CF /. +Arguments cfnorm {gT B%g} phi%CF /. Notation "''CF' ( G )" := (classfun G) : type_scope. Notation "''CF' ( G )" := (@fullv _ (cfun_vectType G)) : vspace_scope. @@ -414,8 +415,6 @@ Notation "''[' u , v ]_ G":= (@cfdot _ G u v) (only parsing) : ring_scope. Notation "''[' u , v ]" := (cfdot u v) : ring_scope. Notation "''[' u ]_ G" := '[u, u]_G (only parsing) : ring_scope. Notation "''[' u ]" := '[u, u] : ring_scope. -Notation cfdotr := (cfdotr_head tt). -Notation cfnorm := (cfnorm_head tt). Section Predicates. diff --git a/mathcomp/solvable/gfunctor.v b/mathcomp/solvable/gfunctor.v index 2fcb8ac..1f8c26f 100644 --- a/mathcomp/solvable/gfunctor.v +++ b/mathcomp/solvable/gfunctor.v @@ -148,7 +148,7 @@ Definition monotonic := Variables (k : unit) (F1 F2 : object_map). -Definition comp_head : object_map := fun gT A => let: tt := k in F1 (F2 A). +Definition comp : object_map := fun gT A => F1 (F2 A). Definition modulo : object_map := fun gT A => coset (F2 A) @*^-1 (F1 (A / (F2 A))). @@ -244,7 +244,8 @@ Export GFunctor.Exports. Bind Scope gFun_scope with GFunctor.object_map. -Notation "F1 \o F2" := (GFunctor.comp_head tt F1 F2) : gFun_scope. +Arguments GFunctor.comp F1 F2 _ /. +Notation "F1 \o F2" := (GFunctor.comp F1 F2) : gFun_scope. Notation "F1 %% F2" := (GFunctor.modulo F1 F2) : gFun_scope. Section FunctorGroup. |