OAI/Analysis/WeakInfiniteness/ReducedGroupAlgebra.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.WeakPureInfiniteness.groupHilbertNontrivial line 22
  2. abbrev OAI.WeakPureInfiniteness.leftRegularRepresentation line 29
  3. def OAI.WeakPureInfiniteness.reducedGroupSubalgebra line 33
  4. abbrev OAI.WeakPureInfiniteness.ReducedGroupAlgebra line 37
  5. lemma OAI.WeakPureInfiniteness.reducedGroupSubalgebra_closed line 39
  6. instance OAI.WeakPureInfiniteness.(instance at line 43) line 43
  7. def OAI.WeakPureInfiniteness.fullToReduced line 48
  8. lemma OAI.WeakPureInfiniteness.fullToReduced_surjective line 51
  9. lemma OAI.WeakPureInfiniteness.fullToReduced_element line 58
  10. def OAI.WeakPureInfiniteness.fullGroupAmbientEvaluation line 62
  11. lemma OAI.WeakPureInfiniteness.reducedGroupSubalgebra_eq_closedStarSpan line 72