OAI/NumberTheory/TotientAsymptotic/InitialRoughEncoding.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Extracting the largest prime in the first, large rough factor.

  1. structure OAI.TotientAsymptotic.InitialRoughConditions line 10
  2. def OAI.TotientAsymptotic.initialRoughEncoding line 22
  3. lemma OAI.TotientAsymptotic.initial_rough_two line 24
  4. lemma OAI.TotientAsymptotic.initial_rough_log_largest line 31
  5. lemma OAI.TotientAsymptotic.initial_rough_product line 46
  6. lemma OAI.TotientAsymptotic.initial_rough_injOn line 51
  7. lemma OAI.TotientAsymptotic.initial_rough_residual line 58