Metamath Blueprint : AKS (PRIMES is in P)
Theorem
aks61c7
Status:
Draft
Reference:
Claim 2 from ~ https://www3.nd.edu/%7eandyp/notes/AKS.pdf