OAI/NumberTheory/TotientAsymptotic/DistinctPrimeRemoval.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The two cross-prime removals in the unequal-largest-prime case.

  1. lemma OAI.TotientAsymptotic.other_prime_dvd_divideFactor line 11
  2. def OAI.TotientAsymptotic.doubleDivide line 24
  3. def OAI.TotientAsymptotic.doubleMultiply line 27
  4. lemma OAI.TotientAsymptotic.doubleMultiply_doubleDivide line 30
  5. lemma OAI.TotientAsymptotic.prod_doubleDivide line 36
  6. lemma OAI.TotientAsymptotic.doubleDivide_prod_dvd line 42
  7. lemma OAI.TotientAsymptotic.doubleDivide_prod_pos line 47
  8. lemma OAI.TotientAsymptotic.distinct_largest_cross_slots line 52