OAI/NumberTheory/Ostmann/Arithmetic/MovingIntegerCells.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The literal moving arithmetic and spectator weights for integer giants

  1. theorem OAI.Ostmann.complexIntegerInterval_congr line 12
  2. theorem OAI.Ostmann.movingSupportedIntegerInterval_cells line 23
  3. theorem OAI.Ostmann.moving_supported_integer_comparison line 49
  4. theorem OAI.Ostmann.moving_spectator_integer_comparison line 78