OAI/Analysis/LaughlinFock/Rotations.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Rotations.

  1. theorem OAI.LaughlinFock.matrix_unitary_isClosed line 12
  2. theorem OAI.LaughlinFock.unitaryMatrix_compactSpace line 20
  3. def OAI.LaughlinFock.unitaryConjugation line 32
  4. theorem OAI.LaughlinFock.unitaryConjugation_one line 36
  5. theorem OAI.LaughlinFock.unitaryConjugation_mul line 40
  6. theorem OAI.LaughlinFock.unitaryConjugation_inv_cancel line 45
  7. abbrev OAI.LaughlinFock.UnitaryFamily line 55
  8. def OAI.LaughlinFock.covarianceSubgroup line 59
  9. theorem OAI.LaughlinFock.covarianceSubgroup_isClosed line 81
  10. theorem OAI.LaughlinFock.rotation_exp_unitary line 107
  11. def OAI.LaughlinFock.rotationFlow line 127
  12. theorem OAI.LaughlinFock.rotationFlow_conjugation line 131
  13. def OAI.LaughlinFock.rotationGroup line 143
  14. theorem OAI.LaughlinFock.rotationFlow_mem_group line 147
  15. theorem OAI.LaughlinFock.rotationGroup_covariance line 154
  16. instance OAI.LaughlinFock.rotationGroup_compactSpace line 169