OAI/Analysis/GroupDeterminants/ClosedAlgebra.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.GroupRingDeterminant.complexOperator_single line 13
  2. def OAI.GroupRingDeterminant.finiteGroupAlgebra line 32
  3. theorem OAI.GroupRingDeterminant.elementaryOperator_mem line 35
  4. theorem OAI.GroupRingDeterminant.finiteGroupAlgebra_star line 40
  5. def OAI.GroupRingDeterminant.finiteGroupStarAlgebra line 57
  6. def OAI.GroupRingDeterminant.closedGroupAlgebra line 60
  7. theorem OAI.GroupRingDeterminant.continuous_groupTrace line 63
  8. theorem OAI.GroupRingDeterminant.groupTrace_closed_mul_comm line 69
  9. theorem OAI.GroupRingDeterminant.groupTrace_one line 88