OAI/NumberTheory/TotientAsymptotic/FordBandSupports.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Support, equality and squarefreeness of the actual bands of a Ford tuple.

  1. lemma OAI.TotientAsymptotic.ford_scale_bounds line 11
  2. lemma OAI.TotientAsymptotic.two_le_of_one_lt_largest line 21
  3. def OAI.TotientAsymptotic.fordBand line 26
  4. lemma OAI.TotientAsymptotic.ford_band_tail line 30
  5. lemma OAI.TotientAsymptotic.ford_band_product line 41
  6. lemma OAI.TotientAsymptotic.ford_band_product_eq line 48
  7. lemma OAI.TotientAsymptotic.ford_band_squarefree line 57