OAI/NumberTheory/TotientAsymptotic/CollisionEndpointDomain.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Every retained dyadic endpoint eventually lies in any fixed analytic domain.

  1. theorem OAI.TotientAsymptotic.collision_endpoints_eventually line 13