OAI/NumberTheory/TotientAsymptotic/GaussianTail.lean
1 declarations, 0 contain sorry, 0 declared as axioms
Finite Gaussian tails with the same exponent at the first index.
- lemma
OAI.TotientAsymptotic.finite_gaussian_tailline 10