Hello everyone! Does there exist an implementation of the isomorphism between the quotient of integers mod some n ($Z/n$) and the finite group with n elements ($Z_n=\{0,...,n-1\}$)? More generally, I can't seem to find a connection between the quotient in the fingroup part of math-comp and the quotient in the ssralg part. Does one exist?

Hi! I think you are right and the connexion is missing. Contributions are welcome.

Okay, thanks!

Last updated: Jul 15 2024 at 20:02 UTC