OAI/Analysis/LaughlinGap/Certificate5.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Certificate5.

  1. def OAI.LaughlinGap.RealOccupation.Certificate5.keys line 18
  2. def OAI.LaughlinGap.RealOccupation.Certificate5.fibers line 19
  3. def OAI.LaughlinGap.RealOccupation.Certificate5.columns line 20
  4. def OAI.LaughlinGap.RealOccupation.Certificate5.Y line 21
  5. def OAI.LaughlinGap.RealOccupation.Certificate5.Z line 22
  6. def OAI.LaughlinGap.RealOccupation.Certificate5.W line 23
  7. def OAI.LaughlinGap.RealOccupation.Certificate5.M line 24
  8. def OAI.LaughlinGap.RealOccupation.Certificate5.L line 25
  9. def OAI.LaughlinGap.RealOccupation.Certificate5.diag line 26
  10. lemma OAI.LaughlinGap.RealOccupation.Certificate5.keys_checked line 28
  11. lemma OAI.LaughlinGap.RealOccupation.Certificate5.keys_injective line 29
  12. lemma OAI.LaughlinGap.RealOccupation.Certificate5.fibers_checked_0 line 30
  13. lemma OAI.LaughlinGap.RealOccupation.Certificate5.fibers_checked line 32
  14. lemma OAI.LaughlinGap.RealOccupation.Certificate5.columns_checked_0 line 37
  15. lemma OAI.LaughlinGap.RealOccupation.Certificate5.columns_checked_1 line 40
  16. lemma OAI.LaughlinGap.RealOccupation.Certificate5.columns_checked_2 line 43
  17. lemma OAI.LaughlinGap.RealOccupation.Certificate5.columns_checked line 46
  18. lemma OAI.LaughlinGap.RealOccupation.Certificate5.gram_checked_0 line 52
  19. lemma OAI.LaughlinGap.RealOccupation.Certificate5.gram_checked_1 line 55
  20. lemma OAI.LaughlinGap.RealOccupation.Certificate5.gram_checked_2 line 58
  21. lemma OAI.LaughlinGap.RealOccupation.Certificate5.gram_checked line 61
  22. lemma OAI.LaughlinGap.RealOccupation.Certificate5.rows_table_checked_0 line 67
  23. lemma OAI.LaughlinGap.RealOccupation.Certificate5.rows_table_checked_1 line 70
  24. lemma OAI.LaughlinGap.RealOccupation.Certificate5.rows_table_checked_2 line 73
  25. lemma OAI.LaughlinGap.RealOccupation.Certificate5.rows_table_checked line 76
  26. lemma OAI.LaughlinGap.RealOccupation.Certificate5.rows_checked line 82
  27. lemma OAI.LaughlinGap.RealOccupation.Certificate5.product_checked_0 line 85
  28. lemma OAI.LaughlinGap.RealOccupation.Certificate5.product_checked_1 line 88
  29. lemma OAI.LaughlinGap.RealOccupation.Certificate5.product_checked_2 line 91
  30. lemma OAI.LaughlinGap.RealOccupation.Certificate5.product_checked line 94
  31. lemma OAI.LaughlinGap.RealOccupation.Certificate5.compression_checked_0 line 100
  32. lemma OAI.LaughlinGap.RealOccupation.Certificate5.compression_checked_1 line 103
  33. lemma OAI.LaughlinGap.RealOccupation.Certificate5.compression_checked_2 line 106
  34. lemma OAI.LaughlinGap.RealOccupation.Certificate5.compression_checked line 109
  35. lemma OAI.LaughlinGap.RealOccupation.Certificate5.ldl_checked_0 line 115
  36. lemma OAI.LaughlinGap.RealOccupation.Certificate5.ldl_checked_1 line 118
  37. lemma OAI.LaughlinGap.RealOccupation.Certificate5.ldl_checked_2 line 121
  38. lemma OAI.LaughlinGap.RealOccupation.Certificate5.ldl_checked line 124
  39. lemma OAI.LaughlinGap.RealOccupation.Certificate5.diag_checked line 130
  40. lemma OAI.LaughlinGap.RealOccupation.Certificate5.certificate line 131