diff options
| author | Cyril Cohen | 2020-11-20 03:10:59 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2020-11-20 03:10:59 +0100 |
| commit | 7c47bab45686e90ee50e6c7eaae3230cb7ce9e53 (patch) | |
| tree | 3e90f47d229669b376a967c63b3aa9bb6ad89beb /mathcomp/character | |
| parent | 676a9266ad77232ab198c86a6a3a3f3f6ba53cc0 (diff) | |
Using Arguments / to deal with volatile definitions
Diffstat (limited to 'mathcomp/character')
| -rw-r--r-- | mathcomp/character/character.v | 6 | ||||
| -rw-r--r-- | mathcomp/character/classfun.v | 9 |
2 files changed, 7 insertions, 8 deletions
diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v index e7ea1e0..c45dc07 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 ccfc37b..d9d3476 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. |