`OAI/RingTheory/DirectFiniteness/PrimeCertificate.lean`

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.mersenne_21701_prime line 6
Source documentation
A Lucas–Lehmer certificate for the Mersenne prime used in the degree bound.
```
theorem mersenne_21701_prime : (mersenne 21701).Prime := by
…
```