OAI/Analysis/Quantum/DimensionTen/Mod139Result.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DimensionTen.Mod139.g1 line 8
  2. def OAI.DimensionTen.Mod139.a1 line 10
  3. def OAI.DimensionTen.Mod139.b1 line 12
  4. def OAI.DimensionTen.Mod139.bezout1_t line 14
  5. theorem OAI.DimensionTen.Mod139.bezout1_integer line 16
  6. theorem OAI.DimensionTen.Mod139.bezout1 line 22
  7. def OAI.DimensionTen.Mod139.div1_f line 28
  8. def OAI.DimensionTen.Mod139.factor1_f_t line 30
  9. theorem OAI.DimensionTen.Mod139.factor1_f_integer line 32
  10. theorem OAI.DimensionTen.Mod139.factor1_f line 38
  11. def OAI.DimensionTen.Mod139.div1_u1 line 44
  12. def OAI.DimensionTen.Mod139.factor1_u1_t line 46
  13. theorem OAI.DimensionTen.Mod139.factor1_u1_integer line 48
  14. theorem OAI.DimensionTen.Mod139.factor1_u1 line 54
  15. def OAI.DimensionTen.Mod139.df line 60
  16. def OAI.DimensionTen.Mod139.da line 62
  17. def OAI.DimensionTen.Mod139.db line 64
  18. def OAI.DimensionTen.Mod139.separable_bezout_t line 66
  19. theorem OAI.DimensionTen.Mod139.separable_bezout_integer line 68
  20. theorem OAI.DimensionTen.Mod139.separable_bezout line 74
  21. lemma OAI.DimensionTen.Mod139.horner_monic_degree line 86
  22. lemma OAI.DimensionTen.Mod139.horner_zero_degree line 96
  23. lemma OAI.DimensionTen.Mod139.degree_f line 100
  24. lemma OAI.DimensionTen.Mod139.degree_g line 106
  25. lemma OAI.DimensionTen.Mod139.map_f line 112
  26. lemma OAI.DimensionTen.Mod139.map_g1 line 116
  27. def OAI.DimensionTen.Mod139.derivative_extra line 120
  28. lemma OAI.DimensionTen.Mod139.derivative_identity line 121
  29. lemma OAI.DimensionTen.Mod139.separable_f line 127
  30. lemma OAI.DimensionTen.Mod139.fixed_iff_g_zero line 134