OAI/Analysis/LaughlinFock/FourCopies.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Four Copies.

  1. abbrev OAI.LaughlinFock.FourSpinIndex line 13
  2. abbrev OAI.LaughlinFock.ValidFourCopy line 17
  3. def OAI.LaughlinFock.fourSpinCopyEquiv line 21
  4. def OAI.LaughlinFock.fourSpinDegree line 59
  5. def OAI.LaughlinFock.fourCopyColumns line 63
  6. def OAI.LaughlinFock.fourSpinColumns line 70
  7. theorem OAI.LaughlinFock.fourSpinColumns_eq_copy line 76
  8. def OAI.LaughlinFock.fourCopyWedge line 93
  9. theorem OAI.LaughlinFock.fourCopyWedge_intertwines line 99