OAI/NumberTheory/TotientAsymptotic/LargestPrimeCofactor.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual largest-prime/cofactor decomposition for a nonnormal prime.

  1. lemma OAI.TotientAsymptotic.largestPrimeFactor_mem line 11
  2. lemma OAI.TotientAsymptotic.nonnormal_largest_cofactor line 21