Metamath Blueprint : AKS (PRIMES is in P)

Theorem aks61c1

Metamath Blueprints

Triangle Congruences
AKS (PRIMES is in P)
- intro1
- aks61c6
- rhmextex
- akslb
- aks10kbnd
- aks61c5
- aks61c4
- lcmineqlem
- odrlblem
- aks61c2
- cl3
- aks22
- aks61c7
- aks61c1
- intro2
- aks61
- aks61c3
- claim2p1
- defintrospective
- aksthr
- aksth
- taylconcavebnd
Derivative of real logarithm (iset)

Status:

Formalized

Reference:

Claim 1 from ~ https://www3.nd.edu/%7eandyp/notes/AKS.pdf