OAI/NumberTheory/CubicMoment/Angular/AngularStoppedAllTuples.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The distinguished-role estimate for every finite tuple, including zero distinguished primes. The empty case is an exact vanishing identity.

  1. theorem OAI.CubicFirstMoment.angular_stoppedBeta_distinguished_log_saving_all line 19