OAI/NumberTheory/CubicMoment/Angular/AngularLongPrimeContext.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Largest-prime cancellation with the full fixed complementary prime set. The selected-bin role compares against the primes of both other factors, rather than just those of its own Möbius complement.

  1. theorem OAI.CubicFirstMoment.angular_long_prime_context_moebius_saving line 16