OAI/Analysis/LaughlinGap/SumTable5.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

Sum Table5.

  1. def OAI.LaughlinGap.RealOccupation.SumTable5.s_0_0 line 16
  2. lemma OAI.LaughlinGap.RealOccupation.SumTable5.s_0_0_checked line 17
  3. def OAI.LaughlinGap.RealOccupation.SumTable5.s_0_1 line 21
  4. lemma OAI.LaughlinGap.RealOccupation.SumTable5.s_0_1_checked line 22
  5. def OAI.LaughlinGap.RealOccupation.SumTable5.s_0_2 line 26
  6. lemma OAI.LaughlinGap.RealOccupation.SumTable5.s_0_2_checked line 27
  7. def OAI.LaughlinGap.RealOccupation.SumTable5.s_0_3 line 31
  8. lemma OAI.LaughlinGap.RealOccupation.SumTable5.s_0_3_checked line 32
  9. def OAI.LaughlinGap.RealOccupation.SumTable5.s_0_4 line 36
  10. lemma OAI.LaughlinGap.RealOccupation.SumTable5.s_0_4_checked line 37
  11. def OAI.LaughlinGap.RealOccupation.SumTable5.s_0_5 line 41
  12. lemma OAI.LaughlinGap.RealOccupation.SumTable5.s_0_5_checked line 42
  13. def OAI.LaughlinGap.RealOccupation.SumTable5.s_0_6 line 46
  14. lemma OAI.LaughlinGap.RealOccupation.SumTable5.s_0_6_checked line 47
  15. def OAI.LaughlinGap.RealOccupation.SumTable5.s_0_7 line 51
  16. lemma OAI.LaughlinGap.RealOccupation.SumTable5.s_0_7_checked line 52
  17. def OAI.LaughlinGap.RealOccupation.SumTable5.s_1_0 line 56
  18. lemma OAI.LaughlinGap.RealOccupation.SumTable5.s_1_0_checked line 57
  19. def OAI.LaughlinGap.RealOccupation.SumTable5.s_1_1 line 61
  20. lemma OAI.LaughlinGap.RealOccupation.SumTable5.s_1_1_checked line 62
  21. def OAI.LaughlinGap.RealOccupation.SumTable5.s_1_2 line 66
  22. lemma OAI.LaughlinGap.RealOccupation.SumTable5.s_1_2_checked line 67
  23. def OAI.LaughlinGap.RealOccupation.SumTable5.s_1_3 line 71
  24. lemma OAI.LaughlinGap.RealOccupation.SumTable5.s_1_3_checked line 72
  25. def OAI.LaughlinGap.RealOccupation.SumTable5.s_1_4 line 76
  26. lemma OAI.LaughlinGap.RealOccupation.SumTable5.s_1_4_checked line 77
  27. def OAI.LaughlinGap.RealOccupation.SumTable5.s_1_5 line 81
  28. lemma OAI.LaughlinGap.RealOccupation.SumTable5.s_1_5_checked line 82
  29. def OAI.LaughlinGap.RealOccupation.SumTable5.s_1_6 line 86
  30. lemma OAI.LaughlinGap.RealOccupation.SumTable5.s_1_6_checked line 87
  31. def OAI.LaughlinGap.RealOccupation.SumTable5.s_1_7 line 91
  32. lemma OAI.LaughlinGap.RealOccupation.SumTable5.s_1_7_checked line 92
  33. def OAI.LaughlinGap.RealOccupation.SumTable5.s_2_0 line 96
  34. lemma OAI.LaughlinGap.RealOccupation.SumTable5.s_2_0_checked line 97
  35. def OAI.LaughlinGap.RealOccupation.SumTable5.s_2_1 line 101
  36. lemma OAI.LaughlinGap.RealOccupation.SumTable5.s_2_1_checked line 102
  37. def OAI.LaughlinGap.RealOccupation.SumTable5.s_2_2 line 106
  38. lemma OAI.LaughlinGap.RealOccupation.SumTable5.s_2_2_checked line 107
  39. def OAI.LaughlinGap.RealOccupation.SumTable5.s_2_3 line 111
  40. lemma OAI.LaughlinGap.RealOccupation.SumTable5.s_2_3_checked line 112
  41. def OAI.LaughlinGap.RealOccupation.SumTable5.s_2_4 line 116
  42. lemma OAI.LaughlinGap.RealOccupation.SumTable5.s_2_4_checked line 117
  43. def OAI.LaughlinGap.RealOccupation.SumTable5.s_2_5 line 121
  44. lemma OAI.LaughlinGap.RealOccupation.SumTable5.s_2_5_checked line 122
  45. def OAI.LaughlinGap.RealOccupation.SumTable5.s_2_6 line 126
  46. lemma OAI.LaughlinGap.RealOccupation.SumTable5.s_2_6_checked line 127
  47. def OAI.LaughlinGap.RealOccupation.SumTable5.s_2_7 line 131
  48. lemma OAI.LaughlinGap.RealOccupation.SumTable5.s_2_7_checked line 132
  49. def OAI.LaughlinGap.RealOccupation.SumTable5.sums line 136
  50. lemma OAI.LaughlinGap.RealOccupation.SumTable5.sums_checked line 137