OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternSpectatorUnits.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The spectator unit conditions from the actual pattern coordinates

  1. theorem OAI.Ostmann.movingSlotValues_unit line 11
  2. theorem OAI.Ostmann.MovingSampleSlots.values_units_of_coordinates line 21
  3. theorem OAI.Ostmann.movingPatternFiniteSamples_units line 35
  4. theorem OAI.Ostmann.movingPatternFiniteSmall_unit line 45