OAI/NumberTheory/TotientAsymptotic/TotientPreimageBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Concrete preimage bounds for the finite totient counting reductions.

  1. lemma OAI.TotientAsymptotic.prime_le_shift_square line 10
  2. lemma OAI.TotientAsymptotic.radical_le_twice_shift_product_square line 15
  3. lemma OAI.TotientAsymptotic.totient_preimage_quadratic line 34