OAI/NumberTheory/TotientAsymptotic/RemovePrimeFactor.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Removing one designated prime from a factorization and reconstructing it.

  1. def OAI.TotientAsymptotic.divideFactor line 11
  2. lemma OAI.TotientAsymptotic.multiply_divideFactor line 14
  3. lemma OAI.TotientAsymptotic.prod_divideFactor line 22
  4. lemma OAI.TotientAsymptotic.divideFactor_prod_dvd line 26
  5. lemma OAI.TotientAsymptotic.divideFactor_prod_pos line 30
  6. lemma OAI.TotientAsymptotic.divideFactor_prod_omega_le line 38
  7. lemma OAI.TotientAsymptotic.divideFactor_prod_factors line 43