OAI/NumberTheory/TotientAsymptotic/BootstrapRealGaussian.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Transfer the explicit preliminary exception to every real endpoint.

  1. theorem OAI.TotientAsymptotic.bootstrap_good_real_gaussian line 13
  2. lemma OAI.TotientAsymptotic.bootstrap_floor_good_large_head line 75