OAI/Analysis/Laughlin/FourBody/Basic.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Laughlin.Certificate.V line 11
  2. def OAI.Laughlin.Certificate.yEntry line 14
  3. def OAI.Laughlin.Certificate.yRow line 27
  4. def OAI.Laughlin.Certificate.Y line 30
  5. theorem OAI.Laughlin.Certificate.Y_expand line 33
  6. def OAI.Laughlin.Certificate.quadruples line 39
  7. def OAI.Laughlin.Certificate.L line 46
  8. def OAI.Laughlin.Certificate.Z line 55
  9. def OAI.Laughlin.Certificate.copyLabel line 61
  10. def OAI.Laughlin.Certificate.gramRational line 63
  11. def OAI.Laughlin.Certificate.errorRational line 66
  12. theorem OAI.Laughlin.Certificate.gram_five line 70