OAI/Analysis/Laughlin/Fock/Annihilation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Laughlin.Fock.insertionSign line 7
2. theorem OAI.Laughlin.Fock.insertionSign_spec line 10
3. theorem OAI.Laughlin.Fock.insertionSign_sq line 16
4. theorem OAI.Laughlin.Fock.insertionSign_norm line 20
5. theorem OAI.Laughlin.Fock.create_unoccupied line 24
6. theorem OAI.Laughlin.Fock.annihilate_insert line 29
7. theorem OAI.Laughlin.Fock.annihilate_occupied line 40
8. theorem OAI.Laughlin.Fock.number_occupation line 47