OAI/NumberTheory/TotientAsymptotic/NormalityThreshold.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Explicit elementary conditions above one fixed endpoint threshold.

  1. lemma OAI.TotientAsymptotic.normality_threshold_conditions line 9
  2. lemma OAI.TotientAsymptotic.normality_large_S_threshold line 20