OAI/Analysis/LaughlinFock/CopyVectors.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Copy Vectors.

  1. theorem OAI.LaughlinFock.pairAnnihilator_increasing line 12
  2. theorem OAI.LaughlinFock.wedgeCoupledCoefficient_one_eq_pair line 22
  3. def OAI.LaughlinFock.wideFourWedgeMatrix line 30
  4. theorem OAI.LaughlinFock.wideFourAnnihilator_mem line 35
  5. theorem OAI.LaughlinFock.wideFourWedgeMatrix_annihilator_column line 41
  6. def OAI.LaughlinFock.composedFourWedgeColumn line 48
  7. def OAI.LaughlinFock.composedFourAnnihilator line 52
  8. theorem OAI.LaughlinFock.composedFourAnnihilator_eq_wedge line 56
  9. theorem OAI.LaughlinFock.highestFourAnnihilator_eq_composed line 65
  10. theorem OAI.LaughlinFock.highestFourAnnihilator_eq_wedge line 86
  11. theorem OAI.LaughlinFock.composedFourAnnihilator_one line 93
  12. theorem OAI.LaughlinFock.annihilatorVector_wedgeAnnihilator line 117
  13. theorem OAI.LaughlinFock.wedgeAnnihilator_injective line 126
  14. theorem OAI.LaughlinFock.composedFourWedgeColumn_one line 133
  15. theorem OAI.LaughlinFock.fourCoupledWedgeMatrix_even_deficit_zero line 142