OAI/NumberTheory/TotientAsymptotic/SeedArithmetic.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Elementary discharge of the finite least-preimage seed.

  1. lemma OAI.TotientAsymptotic.seed_prime_choices line 12
  2. lemma OAI.TotientAsymptotic.seed_preimage_prime_choices line 23
  3. lemma OAI.TotientAsymptotic.seed_isTotient line 31