OAI/NumberTheory/TotientAsymptotic/FordLargestPrime.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The leading Ford prime is exactly the largest prime factor, with padding 1.

  1. lemma OAI.TotientAsymptotic.fordPrime_zero_eq_largest line 9