OAI/NumberTheory/TotientAsymptotic/SeedMinimum.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TotientAsymptotic.seed_preimage_even line 10
2. lemma OAI.TotientAsymptotic.seed_preimage_lower line 65
3. theorem OAI.TotientAsymptotic.seed_least_preimage line 98

   Source documentation

   Exact published seed calculation, proved by finite prime-choice reduction and Euler's product formula rather than an exhaustive search over integers.

   theorem seed_least_preimage : ell (2^18*257)=135268352 := by
   …

   Mentions: OAI.TotientAsymptotic.ell