Commit 2023-12-12 23:03 a6c8a980

feat: primality criteria for Monoid.exponent (#8723) This PR shows a few facts related to Monoid.exponent, especially when it is prime:

1. A nontrivial finite cancellative monoid has exponent greater than 1.
2. A nontrivial monoid has prime exponent p if and only if every non-identity element has order p.
3. A group of order p ^ 2 with p prime is not cyclic if and only if it has exponent p.