OAI/Analysis/WeakInfiniteness/FullGroupAlgebra.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakPureInfiniteness.closedStarSpan line 16
  2. lemma OAI.WeakPureInfiniteness.closedStarSpan_closed line 19
  3. lemma OAI.WeakPureInfiniteness.subset_closedStarSpan line 22
  4. lemma OAI.WeakPureInfiniteness.closedStarSpan_le line 26
  5. def OAI.WeakPureInfiniteness.closedStarSpanCStar line 33
  6. structure OAI.WeakPureInfiniteness.GroupRepresentation line 38
  7. def OAI.WeakPureInfiniteness.FullGroupAmbient line 45
  8. instance OAI.WeakPureInfiniteness.(instance at line 48) line 48
  9. instance OAI.WeakPureInfiniteness.(instance at line 52) line 52
  10. def OAI.WeakPureInfiniteness.fullGroupOperator line 57
  11. lemma OAI.WeakPureInfiniteness.fullGroupOperator_one line 62
  12. lemma OAI.WeakPureInfiniteness.fullGroupOperator_mul line 68
  13. lemma OAI.WeakPureInfiniteness.fullGroupOperator_inv line 75
  14. def OAI.WeakPureInfiniteness.fullGroupSubalgebra line 82
  15. def OAI.WeakPureInfiniteness.FullGroupAlgebra line 85
  16. instance OAI.WeakPureInfiniteness.(instance at line 87) line 87
  17. def OAI.WeakPureInfiniteness.fullGroupElement line 89
  18. lemma OAI.WeakPureInfiniteness.fullGroupElement_one line 93
  19. lemma OAI.WeakPureInfiniteness.fullGroupElement_mul line 97
  20. lemma OAI.WeakPureInfiniteness.fullGroupElement_inv line 102
  21. lemma OAI.WeakPureInfiniteness.fullGroupElement_unitary line 105
  22. def OAI.WeakPureInfiniteness.fullGroupUnitary line 110
  23. def OAI.WeakPureInfiniteness.fullGroupEvaluation line 115
  24. lemma OAI.WeakPureInfiniteness.fullGroupEvaluation_element line 126
  25. lemma OAI.WeakPureInfiniteness.norm_fullGroup_le_iff line 129
  26. lemma OAI.WeakPureInfiniteness.fullGroupEvaluation_separates line 138