OAI/NumberTheory/SingleFold/PolynomialCompiler.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SingleFold.Compiler.elim_comp_map line 7
  2. lemma OAI.SingleFold.Compiler.elim_comp_assoc line 12
  3. structure OAI.SingleFold.Compiler.Representation line 17
  4. def OAI.SingleFold.Compiler.SF line 27
  5. def OAI.SingleFold.Compiler.Representation.congr line 32
  6. def OAI.SingleFold.Compiler.Representation.atom line 40
  7. def OAI.SingleFold.Compiler.Representation.reindex line 48
  8. def OAI.SingleFold.Compiler.Representation.and line 57
  9. def OAI.SingleFold.Compiler.Representation.ex line 90
  10. def OAI.SingleFold.Compiler.Representation.zeros line 115
  11. lemma OAI.SingleFold.Compiler.Representation.zeros_eq line 120
  12. def OAI.SingleFold.Compiler.Representation.or line 128
  13. def OAI.SingleFold.Compiler.Representation.allFin line 195
  14. def OAI.SingleFold.Compiler.Representation.all line 201
  15. def OAI.SingleFold.Compiler.Representation.eq line 211
  16. def OAI.SingleFold.Compiler.Representation.le line 214
  17. def OAI.SingleFold.Compiler.Representation.lt line 235
  18. theorem OAI.SingleFold.Compiler.poly_to_mv line 240
  19. theorem OAI.SingleFold.Compiler.export_polynomial line 254