OAI/Analysis/GroupDeterminants/ComplexRepresentation.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GroupRingDeterminant.shiftFunctions line 13
  2. def OAI.GroupRingDeterminant.convolutionHom line 21
  3. theorem OAI.GroupRingDeterminant.convolutionHom_apply line 24
  4. def OAI.GroupRingDeterminant.complexOperator line 36
  5. theorem OAI.GroupRingDeterminant.complexOperator_apply line 41
  6. theorem OAI.GroupRingDeterminant.complexOperator_curry line 55
  7. theorem OAI.GroupRingDeterminant.complexOperator_mul line 66
  8. theorem OAI.GroupRingDeterminant.complexOperator_one line 78
  9. theorem OAI.GroupRingDeterminant.complexOperator_add line 89
  10. theorem OAI.GroupRingDeterminant.complexOperator_zero line 101
  11. def OAI.GroupRingDeterminant.complexRepresentation line 105
  12. theorem OAI.GroupRingDeterminant.complexOperator_isUnit line 113
  13. theorem OAI.GroupRingDeterminant.complexOperator_integer line 116
  14. theorem OAI.GroupRingDeterminant.regularOperator_isUnit line 131
  15. def OAI.GroupRingDeterminant.groupTraceCLM line 145
  16. theorem OAI.GroupRingDeterminant.groupTraceCLM_apply line 149
  17. theorem OAI.GroupRingDeterminant.groupTrace_complex line 153
  18. theorem OAI.GroupRingDeterminant.coefficient_mul_comm line 172
  19. theorem OAI.GroupRingDeterminant.groupTrace_complex_mul_comm line 177