OAI/Analysis/InterpolatedFactors/Rotations.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FreeGroupFactorMain.CircularRotation.q line 10
  2. theorem OAI.FreeGroupFactorMain.CircularRotation.q_star line 12
  3. theorem OAI.FreeGroupFactorMain.CircularRotation.q_sq line 15
  4. theorem OAI.FreeGroupFactorMain.CircularRotation.two_q_mul line 21
  5. theorem OAI.FreeGroupFactorMain.CircularRotation.qI_star line 26
  6. def OAI.FreeGroupFactorMain.CircularRotation.plus line 34
  7. def OAI.FreeGroupFactorMain.CircularRotation.minus line 35
  8. theorem OAI.FreeGroupFactorMain.CircularRotation.plus_add_minus line 38
  9. theorem OAI.FreeGroupFactorMain.CircularRotation.plus_sub_minus line 44
  10. theorem OAI.FreeGroupFactorMain.CircularRotation.paired_plus line 53
  11. theorem OAI.FreeGroupFactorMain.CircularRotation.paired_minus line 57
  12. theorem OAI.FreeGroupFactorMain.CircularRotation.generation line 61
  13. theorem OAI.FreeGroupFactorMain.CircularRotation.contraction line 75
  14. def OAI.FreeGroupFactorMain.CircularRotation.realFirst line 98
  15. def OAI.FreeGroupFactorMain.CircularRotation.realSecond line 99
  16. theorem OAI.FreeGroupFactorMain.CircularRotation.inverse_paired line 101
  17. theorem OAI.FreeGroupFactorMain.CircularRotation.inverse_contraction line 114
  18. abbrev OAI.FreeGroupFactorMain.CircularRotation.PairedIndex line 131
  19. def OAI.FreeGroupFactorMain.CircularRotation.flip line 133
  20. def OAI.FreeGroupFactorMain.CircularRotation.rotate line 137
  21. theorem OAI.FreeGroupFactorMain.CircularRotation.rotate_covariance line 142
  22. theorem OAI.FreeGroupFactorMain.CircularRotation.rotate_generation line 164