OAI/NumberTheory/TotientAsymptotic/SmoothCountingSplit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A finite counting version of the elementary smooth-number Rankin bound.

  1. lemma OAI.TotientAsymptotic.card_le_endpoint_reciprocal line 11
  2. lemma OAI.TotientAsymptotic.smooth_counting_split line 23