OAI/Combinatorics/SumProduct/Alignment/RegularResidue01.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RegularBoxPartition.left line 25
  2. def OAI.RegularBoxPartition.right line 26
  3. lemma OAI.RegularBoxPartition.normalized line 28
  4. theorem OAI.RegularBoxPartition.one_dimensional line 58
  5. lemma OAI.RegularBoxPartition.endpoints line 84
  6. theorem OAI.RegularBoxPartition.multidimensional line 103
  7. theorem OAI.RegularBoxPartition.fine_partition line 117
  8. def OAI.RegularResiduePieces.cell line 149
  9. lemma OAI.RegularResiduePieces.cell_eq_iff line 156
  10. def OAI.RegularResiduePieces.label line 164
  11. lemma OAI.RegularResiduePieces.label_correct line 168
  12. lemma OAI.RegularResiduePieces.exists_parameters line 182
  13. lemma OAI.RegularResiduePieces.fiber_eq line 187
  14. lemma OAI.RegularResiduePieces.weight_eq line 216
  15. theorem OAI.RegularResiduePieces.actual_weight_error line 227
  16. theorem OAI.RegularResiduePieces.select_common_piece line 260