OAI/Analysis/Quantum/DimensionTen/Mod131Result.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DimensionTen.Mod131.g17 line 8
  2. def OAI.DimensionTen.Mod131.a17 line 10
  3. def OAI.DimensionTen.Mod131.b17 line 12
  4. def OAI.DimensionTen.Mod131.bezout17_t line 14
  5. theorem OAI.DimensionTen.Mod131.bezout17_integer line 16
  6. theorem OAI.DimensionTen.Mod131.bezout17 line 22
  7. def OAI.DimensionTen.Mod131.div17_f line 28
  8. def OAI.DimensionTen.Mod131.factor17_f_t line 30
  9. theorem OAI.DimensionTen.Mod131.factor17_f_integer line 32
  10. theorem OAI.DimensionTen.Mod131.factor17_f line 38
  11. def OAI.DimensionTen.Mod131.div17_u17 line 44
  12. def OAI.DimensionTen.Mod131.factor17_u17_t line 46
  13. theorem OAI.DimensionTen.Mod131.factor17_u17_integer line 48
  14. theorem OAI.DimensionTen.Mod131.factor17_u17 line 54
  15. def OAI.DimensionTen.Mod131.df line 60
  16. def OAI.DimensionTen.Mod131.da line 62
  17. def OAI.DimensionTen.Mod131.db line 64
  18. def OAI.DimensionTen.Mod131.separable_bezout_t line 66
  19. theorem OAI.DimensionTen.Mod131.separable_bezout_integer line 68
  20. theorem OAI.DimensionTen.Mod131.separable_bezout line 74
  21. lemma OAI.DimensionTen.Mod131.horner_monic_degree line 86
  22. lemma OAI.DimensionTen.Mod131.degree_f line 96
  23. lemma OAI.DimensionTen.Mod131.degree_g line 102
  24. lemma OAI.DimensionTen.Mod131.map_f line 108
  25. lemma OAI.DimensionTen.Mod131.map_g17 line 112
  26. def OAI.DimensionTen.Mod131.derivative_extra line 116
  27. lemma OAI.DimensionTen.Mod131.derivative_identity line 117
  28. lemma OAI.DimensionTen.Mod131.separable_f line 123
  29. lemma OAI.DimensionTen.Mod131.fixed_iff_g_zero line 130