OAI/Analysis/GroupDeterminants/TransferAlgebra.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GroupRingDeterminant.projectionReweight line 15
  2. theorem OAI.GroupRingDeterminant.projectionReweight_mul line 17
  3. theorem OAI.GroupRingDeterminant.projectionReweight_one line 29
  4. def OAI.GroupRingDeterminant.projectionReweightUnit line 32
  5. def OAI.GroupRingDeterminant.lowerShear line 44
  6. def OAI.GroupRingDeterminant.upperShear line 47
  7. theorem OAI.GroupRingDeterminant.lowerShear_neg line 50
  8. theorem OAI.GroupRingDeterminant.upperShear_neg line 53
  9. def OAI.GroupRingDeterminant.lowerShearUnit line 56
  10. def OAI.GroupRingDeterminant.upperShearUnit line 62
  11. def OAI.GroupRingDeterminant.blockDiagonalUnit line 68
  12. def OAI.GroupRingDeterminant.transferMatrix line 81
  13. theorem OAI.GroupRingDeterminant.transferMatrix_factorization line 85
  14. theorem OAI.GroupRingDeterminant.transferMatrix_isUnit line 102