OAI/NumberTheory/SingleFold/FunctionalCompiler.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SingleFold.Compiler.MapSF line 7
  2. lemma OAI.SingleFold.Compiler.MapSF.congr line 11
  3. lemma OAI.SingleFold.Compiler.MapSF.proj line 13
  4. lemma OAI.SingleFold.Compiler.MapSF.const line 20
  5. lemma OAI.SingleFold.Compiler.MapSF.reindex line 27
  6. lemma OAI.SingleFold.Compiler.MapSF.comp line 30
  7. lemma OAI.SingleFold.Compiler.MapSF.pair line 42
  8. lemma OAI.SingleFold.Compiler.MapSF.all line 54
  9. lemma OAI.SingleFold.Compiler.MapSF.pullback line 62
  10. def OAI.SingleFold.PointCompiler.Code.decode line 74
  11. lemma OAI.SingleFold.PointCompiler.decode_encode line 77
  12. lemma OAI.SingleFold.PointCompiler.normalized_graph line 79
  13. def OAI.SingleFold.PointCompiler.PointSF line 94
  14. lemma OAI.SingleFold.PointCompiler.PointSF.const line 97
  15. lemma OAI.SingleFold.PointCompiler.PointSF.var line 98
  16. lemma OAI.SingleFold.PointCompiler.PointSF.reindex line 100
  17. lemma OAI.SingleFold.PointCompiler.PointSF.add line 102
  18. lemma OAI.SingleFold.PointCompiler.PointSF.smul line 126
  19. lemma OAI.SingleFold.PointCompiler.PointSF.height line 142
  20. def OAI.SingleFold.Compiler.ScalarSF line 161
  21. lemma OAI.SingleFold.Compiler.ScalarSF.const line 164
  22. lemma OAI.SingleFold.Compiler.ScalarSF.proj line 165
  23. lemma OAI.SingleFold.Compiler.ScalarSF.poly line 166
  24. lemma OAI.SingleFold.Compiler.ScalarSF.add line 173
  25. lemma OAI.SingleFold.Compiler.ScalarSF.mul line 177
  26. lemma OAI.SingleFold.Compiler.ScalarSF.pow line 181
  27. lemma OAI.SingleFold.Compiler.ScalarSF.max line 189
  28. lemma OAI.SingleFold.Compiler.ScalarSF.le line 198
  29. lemma OAI.SingleFold.Compiler.ScalarSF.lt line 204
  30. lemma OAI.SingleFold.Compiler.ScalarSF.eq line 210
  31. lemma OAI.SingleFold.PointCompiler.exprLe_semi line 221
  32. lemma OAI.SingleFold.PointCompiler.PointSF.nonzero line 226
  33. lemma OAI.SingleFold.PointCompiler.PointSF.xle line 232
  34. lemma OAI.SingleFold.PointCompiler.PointSF.ynonneg line 251