OAI/Analysis/Laughlin/FiniteFlux/GramData09.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Laughlin.Certificate.source_error_9_1_1 line 12
  2. theorem OAI.Laughlin.Certificate.source_error_9_1_3 line 23
  3. theorem OAI.Laughlin.Certificate.source_error_9_1_5 line 34
  4. theorem OAI.Laughlin.Certificate.source_error_9_1_7 line 45
  5. theorem OAI.Laughlin.Certificate.source_error_9_1_9 line 56
  6. theorem OAI.Laughlin.Certificate.source_error_9_3_3 line 67
  7. theorem OAI.Laughlin.Certificate.source_error_9_3_5 line 78
  8. theorem OAI.Laughlin.Certificate.source_error_9_3_7 line 89
  9. theorem OAI.Laughlin.Certificate.source_error_9_3_9 line 100
  10. theorem OAI.Laughlin.Certificate.source_error_9_5_5 line 111
  11. theorem OAI.Laughlin.Certificate.source_error_9_5_7 line 122
  12. theorem OAI.Laughlin.Certificate.source_error_9_5_9 line 133
  13. theorem OAI.Laughlin.Certificate.source_error_9_7_7 line 144
  14. theorem OAI.Laughlin.Certificate.source_error_9_7_9 line 155
  15. theorem OAI.Laughlin.Certificate.source_error_9_9_9 line 166
  16. theorem OAI.Laughlin.Certificate.source_gram_9_1_1 line 177
  17. theorem OAI.Laughlin.Certificate.source_gram_9_1_3 line 181
  18. theorem OAI.Laughlin.Certificate.source_gram_9_1_5 line 185
  19. theorem OAI.Laughlin.Certificate.source_gram_9_1_7 line 189
  20. theorem OAI.Laughlin.Certificate.source_gram_9_1_9 line 193
  21. theorem OAI.Laughlin.Certificate.source_gram_9_3_3 line 197
  22. theorem OAI.Laughlin.Certificate.source_gram_9_3_5 line 201
  23. theorem OAI.Laughlin.Certificate.source_gram_9_3_7 line 205
  24. theorem OAI.Laughlin.Certificate.source_gram_9_3_9 line 209
  25. theorem OAI.Laughlin.Certificate.source_gram_9_5_5 line 213
  26. theorem OAI.Laughlin.Certificate.source_gram_9_5_7 line 217
  27. theorem OAI.Laughlin.Certificate.source_gram_9_5_9 line 221
  28. theorem OAI.Laughlin.Certificate.source_gram_9_7_7 line 225
  29. theorem OAI.Laughlin.Certificate.source_gram_9_7_9 line 229
  30. theorem OAI.Laughlin.Certificate.source_gram_9_9_9 line 233
  31. theorem OAI.Laughlin.Certificate.source_error_9_3_1 line 237
  32. theorem OAI.Laughlin.Certificate.source_gram_9_3_1 line 241
  33. theorem OAI.Laughlin.Certificate.source_error_9_5_1 line 245
  34. theorem OAI.Laughlin.Certificate.source_gram_9_5_1 line 249
  35. theorem OAI.Laughlin.Certificate.source_error_9_5_3 line 253
  36. theorem OAI.Laughlin.Certificate.source_gram_9_5_3 line 257
  37. theorem OAI.Laughlin.Certificate.source_error_9_7_1 line 261
  38. theorem OAI.Laughlin.Certificate.source_gram_9_7_1 line 265
  39. theorem OAI.Laughlin.Certificate.source_error_9_7_3 line 269
  40. theorem OAI.Laughlin.Certificate.source_gram_9_7_3 line 273
  41. theorem OAI.Laughlin.Certificate.source_error_9_7_5 line 277
  42. theorem OAI.Laughlin.Certificate.source_gram_9_7_5 line 281
  43. theorem OAI.Laughlin.Certificate.source_error_9_9_1 line 285
  44. theorem OAI.Laughlin.Certificate.source_gram_9_9_1 line 289
  45. theorem OAI.Laughlin.Certificate.source_error_9_9_3 line 293
  46. theorem OAI.Laughlin.Certificate.source_gram_9_9_3 line 297
  47. theorem OAI.Laughlin.Certificate.source_error_9_9_5 line 301
  48. theorem OAI.Laughlin.Certificate.source_gram_9_9_5 line 305
  49. theorem OAI.Laughlin.Certificate.source_error_9_9_7 line 309
  50. theorem OAI.Laughlin.Certificate.source_gram_9_9_7 line 313
  51. theorem OAI.Laughlin.Certificate.error_9 line 317
  52. theorem OAI.Laughlin.Certificate.gram_9 line 346