OAI/Analysis/Laughlin/Fock/Inner.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Laughlin.Fock.occupationInner_smul_left line 8
  2. theorem OAI.Laughlin.Fock.occupationInner_smul_right line 12
  3. theorem OAI.Laughlin.Fock.occupationInner_sum_left line 16
  4. theorem OAI.Laughlin.Fock.occupationInner_sum_right line 22
  5. theorem OAI.Laughlin.Fock.occupationInner_self line 28
  6. theorem OAI.Laughlin.Fock.occupationNormSq_eq_zero line 37