OAI/NumberTheory/Ostmann/Arithmetic/MovingNodeUnits.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Coefficient units forced by the original local support masks

  1. theorem OAI.Ostmann.movingNodeAtPath_root line 12
  2. theorem OAI.Ostmann.MovingSlotData.frequency_dvd_product line 28
  3. theorem OAI.Ostmann.movingLocalSupport_products_units line 34
  4. theorem OAI.Ostmann.movingSlotWeight_node_localSupport line 51
  5. theorem OAI.Ostmann.movingSample_coefficient_units line 73