OAI/NumberTheory/CubicMoment/Angular/AngularStoppedCubeSW.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Cube frequencies are genuine coprimality exclusions in the angular stopped row. The angular factor occurs only once in the coefficient.

  1. theorem OAI.CubicFirstMoment.angular_stopped_sequence_cube_sw line 15