OAI/NumberTheory/Ostmann/Construction/ScheduledIntegerRigidity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Actual product separation on the retained initial-coefficient support

  1. def OAI.Ostmann.scheduledPivotBound line 10
  2. def OAI.Ostmann.scheduledProductRounding line 13
  3. theorem OAI.Ostmann.scheduledPivotBound_upper line 16
  4. theorem OAI.Ostmann.scheduled_retained_product_exponent line 44
  5. theorem OAI.Ostmann.scheduled_retained_product_rounding line 60
  6. theorem OAI.Ostmann.scheduled_original_retained_product_lower line 78
  7. theorem OAI.Ostmann.scheduled_integer_rigidity line 114