OAI/Analysis/Quantum/DimensionTen/IntegerPolynomials.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DimensionTen.Border.FP line 11
  2. def OAI.DimensionTen.Border.F line 14
  3. lemma OAI.DimensionTen.Border.map_FP line 16
  4. lemma OAI.DimensionTen.Border.F_map line 20
  5. lemma OAI.DimensionTen.Border.horner_int_monic line 23
  6. lemma OAI.DimensionTen.Border.FP_degree line 29
  7. lemma OAI.DimensionTen.Border.F_monic line 35
  8. lemma OAI.DimensionTen.Border.F_degree line 36
  9. lemma OAI.DimensionTen.Border.coef_41_0 line 38
  10. lemma OAI.DimensionTen.Border.coef_41_1 line 39
  11. lemma OAI.DimensionTen.Border.coef_41_2 line 40
  12. lemma OAI.DimensionTen.Border.coef_41_3 line 41
  13. lemma OAI.DimensionTen.Border.coef_41_4 line 42
  14. lemma OAI.DimensionTen.Border.coef_41_5 line 43
  15. lemma OAI.DimensionTen.Border.coef_41_6 line 44
  16. lemma OAI.DimensionTen.Border.coef_41_7 line 45
  17. lemma OAI.DimensionTen.Border.coef_41_8 line 46
  18. lemma OAI.DimensionTen.Border.coef_41_9 line 47
  19. lemma OAI.DimensionTen.Border.coef_41_10 line 48
  20. lemma OAI.DimensionTen.Border.coef_41_11 line 49
  21. lemma OAI.DimensionTen.Border.coef_41_12 line 50
  22. lemma OAI.DimensionTen.Border.coef_41_13 line 51
  23. lemma OAI.DimensionTen.Border.coef_41_14 line 52
  24. lemma OAI.DimensionTen.Border.coef_41_15 line 53
  25. lemma OAI.DimensionTen.Border.coef_41_16 line 54
  26. lemma OAI.DimensionTen.Border.coef_41_17 line 55
  27. lemma OAI.DimensionTen.Border.coef_41_18 line 56
  28. lemma OAI.DimensionTen.Border.coef_41_19 line 57
  29. lemma OAI.DimensionTen.Border.F_reduction_41 line 59
  30. lemma OAI.DimensionTen.Border.coef_131_0 line 64
  31. lemma OAI.DimensionTen.Border.coef_131_1 line 65
  32. lemma OAI.DimensionTen.Border.coef_131_2 line 66
  33. lemma OAI.DimensionTen.Border.coef_131_3 line 67
  34. lemma OAI.DimensionTen.Border.coef_131_4 line 68
  35. lemma OAI.DimensionTen.Border.coef_131_5 line 69
  36. lemma OAI.DimensionTen.Border.coef_131_6 line 70
  37. lemma OAI.DimensionTen.Border.coef_131_7 line 71
  38. lemma OAI.DimensionTen.Border.coef_131_8 line 72
  39. lemma OAI.DimensionTen.Border.coef_131_9 line 73
  40. lemma OAI.DimensionTen.Border.coef_131_10 line 74
  41. lemma OAI.DimensionTen.Border.coef_131_11 line 75
  42. lemma OAI.DimensionTen.Border.coef_131_12 line 76
  43. lemma OAI.DimensionTen.Border.coef_131_13 line 77
  44. lemma OAI.DimensionTen.Border.coef_131_14 line 78
  45. lemma OAI.DimensionTen.Border.coef_131_15 line 79
  46. lemma OAI.DimensionTen.Border.coef_131_16 line 80
  47. lemma OAI.DimensionTen.Border.coef_131_17 line 81
  48. lemma OAI.DimensionTen.Border.coef_131_18 line 82
  49. lemma OAI.DimensionTen.Border.coef_131_19 line 83
  50. lemma OAI.DimensionTen.Border.F_reduction_131 line 85
  51. lemma OAI.DimensionTen.Border.coef_139_0 line 90
  52. lemma OAI.DimensionTen.Border.coef_139_1 line 91
  53. lemma OAI.DimensionTen.Border.coef_139_2 line 92
  54. lemma OAI.DimensionTen.Border.coef_139_3 line 93
  55. lemma OAI.DimensionTen.Border.coef_139_4 line 94
  56. lemma OAI.DimensionTen.Border.coef_139_5 line 95
  57. lemma OAI.DimensionTen.Border.coef_139_6 line 96
  58. lemma OAI.DimensionTen.Border.coef_139_7 line 97
  59. lemma OAI.DimensionTen.Border.coef_139_8 line 98
  60. lemma OAI.DimensionTen.Border.coef_139_9 line 99
  61. lemma OAI.DimensionTen.Border.coef_139_10 line 100
  62. lemma OAI.DimensionTen.Border.coef_139_11 line 101
  63. lemma OAI.DimensionTen.Border.coef_139_12 line 102
  64. lemma OAI.DimensionTen.Border.coef_139_13 line 103
  65. lemma OAI.DimensionTen.Border.coef_139_14 line 104
  66. lemma OAI.DimensionTen.Border.coef_139_15 line 105
  67. lemma OAI.DimensionTen.Border.coef_139_16 line 106
  68. lemma OAI.DimensionTen.Border.coef_139_17 line 107
  69. lemma OAI.DimensionTen.Border.coef_139_18 line 108
  70. lemma OAI.DimensionTen.Border.coef_139_19 line 109
  71. lemma OAI.DimensionTen.Border.F_reduction_139 line 111
  72. lemma OAI.DimensionTen.Border.F_irreducible line 116