diff options
| author | Kazuhiko Sakaguchi | 2020-10-09 00:21:00 +0900 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2020-10-29 12:31:31 +0900 |
| commit | c6e0d703165b0c60c270672eb542aa8934929bfe (patch) | |
| tree | 3ce1b05b861ca60e88bc7ab8b5226b12a879e3e6 /mathcomp/character/mxabelem.v | |
| parent | fe8759d1faec24cbe9d838f777682e260680d370 (diff) | |
Switch from long suffixes to short suffixes
Diffstat (limited to 'mathcomp/character/mxabelem.v')
| -rw-r--r-- | mathcomp/character/mxabelem.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/character/mxabelem.v b/mathcomp/character/mxabelem.v index 92470d9..949ded3 100644 --- a/mathcomp/character/mxabelem.v +++ b/mathcomp/character/mxabelem.v @@ -469,7 +469,7 @@ Local Notation rVn := 'rV['F_p](gval E). Lemma dim_abelemE : n = logn p #|E|. Proof. rewrite /n'; have [_ _ [k ->]] := pgroup_pdiv pE ntE. -by rewrite /pdiv primes_exp ?primes_prime // pfactorK. +by rewrite /pdiv primesX ?primes_prime // pfactorK. Qed. Lemma card_abelem_rV : #|rVn| = #|E|. |