OAI/Analysis/Laughlin/FourBody/PhysicalTrace.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Laughlin.Spin.trace_sandwich_list_sum line 10
2. theorem OAI.Laughlin.Spin.negative_list_sum line 18
3. theorem OAI.Laughlin.Spin.source_fourBody_rows_support line 26
4. theorem OAI.Laughlin.Spin.source_physical_fourBody_trace_identity line 29
5. theorem OAI.Laughlin.Spin.trace_real_sandwich_complex line 51
6. theorem OAI.Laughlin.Spin.physical_fourBody_haar_multiplicity line 59