OAI/Analysis/LaughlinFock/FourTraces.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Four Traces.

  1. theorem OAI.LaughlinFock.composedCoupledVector_eq_sphericalCopy_all line 14
  2. theorem OAI.LaughlinFock.sphericalCopyCoefficient_antisymm line 72
  3. theorem OAI.LaughlinFock.sphericalCopyCoefficient_diagonal line 93
  4. def OAI.LaughlinFock.orderedFourColumn line 100
  5. theorem OAI.LaughlinFock.orderedFourColumn_wedgeAnnihilator line 105
  6. theorem OAI.LaughlinFock.composed_orderedFourColumn_inner line 124
  7. def OAI.LaughlinFock.rowFourPrewedge line 148
  8. theorem OAI.LaughlinFock.exteriorLift_outer_congruence line 156
  9. theorem OAI.LaughlinFock.rowFourPrewedge_lift line 164
  10. theorem OAI.LaughlinFock.outer_bilinear line 188
  11. theorem OAI.LaughlinFock.rowFourPrewedge_coupled_bilinear line 195
  12. def OAI.LaughlinFock.sourceRowFourP line 213
  13. def OAI.LaughlinFock.sourceRowFourKernel line 217
  14. theorem OAI.LaughlinFock.sourceRowFourKernel_lift line 221
  15. theorem OAI.LaughlinFock.sphericalCopyCoefficient_level line 229
  16. theorem OAI.LaughlinFock.rowFour_copyWeight_sum line 235
  17. theorem OAI.LaughlinFock.sourceRowFourKernel_copyTrace line 272