I guess by degree you mean order? And by finiteAbelianGroupOfDegree7 you mean cyclicGroupOfDegree7. Of course, you should always use theorems to keep your notat

I guess by degree you mean order? And by finiteAbelianGroupOfDegree7 you mean cyclicGroupOfDegree7. Of course, you should always use theorems to keep your notation consistent. :)