OAI/Analysis/LaughlinGap/Certificate6.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Certificate6.

  1. def OAI.LaughlinGap.RealOccupation.Certificate6.keys line 16
  2. def OAI.LaughlinGap.RealOccupation.Certificate6.fibers line 17
  3. def OAI.LaughlinGap.RealOccupation.Certificate6.columns line 18
  4. def OAI.LaughlinGap.RealOccupation.Certificate6.Y line 19
  5. def OAI.LaughlinGap.RealOccupation.Certificate6.Z line 20
  6. def OAI.LaughlinGap.RealOccupation.Certificate6.W line 21
  7. def OAI.LaughlinGap.RealOccupation.Certificate6.M line 22
  8. def OAI.LaughlinGap.RealOccupation.Certificate6.L line 23
  9. def OAI.LaughlinGap.RealOccupation.Certificate6.diag line 24
  10. lemma OAI.LaughlinGap.RealOccupation.Certificate6.keys_checked line 26
  11. lemma OAI.LaughlinGap.RealOccupation.Certificate6.keys_injective line 27
  12. lemma OAI.LaughlinGap.RealOccupation.Certificate6.fibers_checked_0 line 28
  13. lemma OAI.LaughlinGap.RealOccupation.Certificate6.fibers_checked line 30
  14. lemma OAI.LaughlinGap.RealOccupation.Certificate6.columns_checked_0 line 35
  15. lemma OAI.LaughlinGap.RealOccupation.Certificate6.columns_checked_1 line 38
  16. lemma OAI.LaughlinGap.RealOccupation.Certificate6.columns_checked_2 line 41
  17. lemma OAI.LaughlinGap.RealOccupation.Certificate6.columns_checked line 44
  18. lemma OAI.LaughlinGap.RealOccupation.Certificate6.gram_checked_0 line 50
  19. lemma OAI.LaughlinGap.RealOccupation.Certificate6.gram_checked_1 line 53
  20. lemma OAI.LaughlinGap.RealOccupation.Certificate6.gram_checked_2 line 56
  21. lemma OAI.LaughlinGap.RealOccupation.Certificate6.gram_checked line 59
  22. lemma OAI.LaughlinGap.RealOccupation.Certificate6.certificate line 65