OAI/Analysis/Laughlin/Pair/CoupledParity.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Laughlin.Spin.sign_reverse line 8
  2. theorem OAI.Laughlin.Spin.highestUnit_reverse line 16
  3. theorem OAI.Laughlin.Spin.genericHighest_swap line 24
  4. theorem OAI.Laughlin.Spin.totalLower_swap line 42
  5. theorem OAI.Laughlin.Spin.genericDescendant_swap line 50
  6. theorem OAI.Laughlin.Spin.genericUnitDescendant_swap line 63
  7. def OAI.Laughlin.Spin.pairCoupledTensor line 69
  8. theorem OAI.Laughlin.Spin.pairCoupledTensor_norm line 72
  9. theorem OAI.Laughlin.Spin.pairCoupledTensor_antisymmetric line 81