diff options
| author | affeldt-aist | 2020-11-20 17:55:19 +0900 |
|---|---|---|
| committer | GitHub | 2020-11-20 17:55:19 +0900 |
| commit | b4cdd47bcd7f2b2f9033ee00b7412570b07b8808 (patch) | |
| tree | 63eaf93913a44ffc2d21c705640af01cdd3bbd17 /mathcomp/character/character.v | |
| parent | 3bb1ccc63170e3e71ef9d5b62758b6fdb1c4371c (diff) | |
| parent | 7c47bab45686e90ee50e6c7eaae3230cb7ce9e53 (diff) | |
Merge pull request #663 from CohenCyril/clean_head
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 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. |