From 7c47bab45686e90ee50e6c7eaae3230cb7ce9e53 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Fri, 20 Nov 2020 03:10:59 +0100 Subject: Using Arguments / to deal with volatile definitions --- mathcomp/character/classfun.v | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) (limited to 'mathcomp/character/classfun.v') 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 := <>%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. -- cgit v1.2.3