OAI/Analysis/Laughlin/FourBody/FockCovariance.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Laughlin.Fock.antisymmetric_exterior_sum line 11
  2. def OAI.Laughlin.Fock.wedgePairVector line 21
  3. theorem OAI.Laughlin.Fock.wedgePairVector_rotation line 24
  4. def OAI.Laughlin.Fock.sourceFourVector line 43
  5. def OAI.Laughlin.Fock.sourceFourFamilyEnd line 46
  6. theorem OAI.Laughlin.Fock.sourceFourVector_adjoint line 49
  7. theorem OAI.Laughlin.Fock.sourceFourVector_rotation line 62
  8. theorem OAI.Laughlin.Fock.sourceFourFamilyEnd_rotation line 71