OAI/Computability/RationalHitting/GridComputation.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RationalHitting.StackLanguage.range_flatMap_to_finRange line 7
  2. theorem OAI.RationalHitting.StackLanguage.Poly.tabulateUp line 14
  3. theorem OAI.RationalHitting.StackLanguage.Poly.flatMapUp line 19
  4. theorem OAI.RationalHitting.StackLanguage.Poly.wordRange line 24
  5. abbrev OAI.RationalHitting.StackLanguage.Runtime.MatrixWordArgs line 35
  6. def OAI.RationalHitting.StackLanguage.Runtime.matrixWord line 37
  7. theorem OAI.RationalHitting.StackLanguage.Runtime.matrixWord_poly line 42
  8. lemma OAI.RationalHitting.StackLanguage.Runtime.matrixWord_of line 52
  9. abbrev OAI.RationalHitting.StackLanguage.Runtime.TupleWordArgs line 67
  10. def OAI.RationalHitting.StackLanguage.Runtime.tupleWord line 69
  11. theorem OAI.RationalHitting.StackLanguage.Runtime.tupleWord_poly line 72
  12. lemma OAI.RationalHitting.StackLanguage.Runtime.tupleWord_eq line 79
  13. def OAI.RationalHitting.StackLanguage.Runtime.point line 111
  14. theorem OAI.RationalHitting.StackLanguage.Runtime.point_poly line 116
  15. lemma OAI.RationalHitting.StackLanguage.Runtime.matrix_det_eq line 127
  16. lemma OAI.RationalHitting.StackLanguage.Runtime.point_eq line 134
  17. lemma OAI.RationalHitting.StackLanguage.map_filterMap_toList line 156
  18. def OAI.RationalHitting.StackLanguage.Runtime.words line 164
  19. theorem OAI.RationalHitting.StackLanguage.Runtime.words_poly line 168
  20. lemma OAI.RationalHitting.StackLanguage.Runtime.gridFn_fin line 175
  21. lemma OAI.RationalHitting.StackLanguage.Runtime.words_eq line 179