OAI/NumberTheory/CubicMoment/Angular/AngularDivisorNoncubeAnnulus.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Noncube saving for a literal square-divisor Poisson block. The principal condition is tested at d*h, as required by the character.

  1. theorem OAI.CubicFirstMoment.angular_divisor_noncube_annulus_saving line 16