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/character.v | |
| parent | 676a9266ad77232ab198c86a6a3a3f3f6ba53cc0 (diff) | |
Using Arguments / to deal with volatile definitions
Diffstat (limited to 'mathcomp/character/character.v')
| -rw-r--r-- | mathcomp/character/character.v | 6 |
1 files changed, 3 insertions, 3 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. |