OAI/Computability/RationalHitting/MatrixComputation.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RationalHitting.StackLanguage.flattenStep line 9
  2. lemma OAI.RationalHitting.StackLanguage.flattenStep_code_le line 12
  3. lemma OAI.RationalHitting.StackLanguage.flattenStep_iterate_code line 25
  4. lemma OAI.RationalHitting.StackLanguage.flattenStep_iterate line 31
  5. theorem OAI.RationalHitting.StackLanguage.Poly.listFlatten line 40
  6. theorem OAI.RationalHitting.StackLanguage.Poly.listFlatMap line 53
  7. instance OAI.RationalHitting.StackLanguage.(instance at line 64) line 64
  8. def OAI.RationalHitting.StackLanguage.concatStep line 66
  9. lemma OAI.RationalHitting.StackLanguage.concatStep_code_le line 69
  10. lemma OAI.RationalHitting.StackLanguage.concatStep_iterate_code line 82
  11. lemma OAI.RationalHitting.StackLanguage.concatStep_iterate line 88
  12. def OAI.RationalHitting.StackLanguage.Procedure.encodeWord line 98
  13. theorem OAI.RationalHitting.StackLanguage.Poly.wordConcat line 119
  14. theorem OAI.RationalHitting.StackLanguage.Poly.encodeNat line 132
  15. theorem OAI.RationalHitting.StackLanguage.Poly.encodeUnary line 136
  16. abbrev OAI.RationalHitting.StackLanguage.Runtime.GridPoint line 145
  17. def OAI.RationalHitting.StackLanguage.Runtime.gridFn line 147
  18. def OAI.RationalHitting.StackLanguage.Runtime.matrix line 149
  19. theorem OAI.RationalHitting.StackLanguage.Runtime.matrix_poly line 152
  20. lemma OAI.RationalHitting.StackLanguage.Runtime.matrix_eq line 159
  21. def OAI.RationalHitting.StackLanguage.Runtime.cramer line 166
  22. theorem OAI.RationalHitting.StackLanguage.Runtime.cramer_poly line 169
  23. lemma OAI.RationalHitting.StackLanguage.Runtime.cramer_of line 187
  24. lemma OAI.RationalHitting.StackLanguage.Runtime.cramer_det_of line 201
  25. lemma OAI.RationalHitting.StackLanguage.Runtime.cramer_encode_of line 209