OAI/Combinatorics/SumProduct/Alignment/RoughProduct01.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RoughProductRemoval.nestedBox line 24
  2. def OAI.RoughProductRemoval.badProduct line 32
  3. def OAI.RoughProductRemoval.productTimes line 42
  4. def OAI.RoughProductRemoval.exceptionalProduct line 45
  5. lemma OAI.RoughProductRemoval.linear_divisibility_class line 65
  6. lemma OAI.RoughProductRemoval.parent_residue line 74
  7. lemma OAI.RoughProductRemoval.parent_vector line 97
  8. lemma OAI.RoughProductRemoval.nestedBox_eq_parent line 108
  9. lemma OAI.RoughProductRemoval.nested_linear_parameter line 124
  10. lemma OAI.RoughProductRemoval.nested_removed_class line 137
  11. lemma OAI.RoughProductRemoval.nestedBox_refine line 146
  12. theorem OAI.RoughProductRemoval.nested_residue_means line 161
  13. def OAI.RoughProductRemoval.firstLift line 211
  14. lemma OAI.RoughProductRemoval.firstLift_degree line 215
  15. lemma OAI.RoughProductRemoval.firstLift_eval line 229
  16. def OAI.RoughProductRemoval.tailLift line 244
  17. lemma OAI.RoughProductRemoval.tailLift_degree line 247
  18. lemma OAI.RoughProductRemoval.tailLift_eval line 258
  19. lemma OAI.RoughProductRemoval.first_polynomial line 265
  20. lemma OAI.RoughProductRemoval.tail_polynomial line 273