OAI/NumberTheory/TotientAsymptotic/SquareInternalDiscard.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

All positive-index squarefree failures, including alternate witnesses.

  1. def OAI.TotientAsymptotic.squareInternalRemainders line 14
  2. lemma OAI.TotientAsymptotic.squareLayerRemainders_basic line 17
  3. lemma OAI.TotientAsymptotic.squareInternalRemainders_basic line 25
  4. lemma OAI.TotientAsymptotic.square_failure_mem_layer line 31
  5. lemma OAI.TotientAsymptotic.square_internal_reciprocal_discard line 71