OAI/Analysis/WeakInfiniteness/GroupRegular.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.WeakPureInfiniteness.GroupHilbert line 15
  2. lemma OAI.WeakPureInfiniteness.mem_l2_reindex line 19
  3. def OAI.WeakPureInfiniteness.l2Reindex line 26
  4. lemma OAI.WeakPureInfiniteness.l2Reindex_apply line 40
  5. lemma OAI.WeakPureInfiniteness.l2Reindex_single line 43
  6. def OAI.WeakPureInfiniteness.leftRegularIsometry line 53
  7. def OAI.WeakPureInfiniteness.rightRegularIsometry line 64
  8. def OAI.WeakPureInfiniteness.leftRegular line 75
  9. def OAI.WeakPureInfiniteness.rightRegular line 78
  10. lemma OAI.WeakPureInfiniteness.leftRegular_apply line 82
  11. lemma OAI.WeakPureInfiniteness.rightRegular_apply line 86
  12. lemma OAI.WeakPureInfiniteness.leftRegular_single line 91
  13. lemma OAI.WeakPureInfiniteness.rightRegular_single line 95
  14. lemma OAI.WeakPureInfiniteness.leftRegular_commute_right line 99
  15. def OAI.WeakPureInfiniteness.groupInversion line 105
  16. lemma OAI.WeakPureInfiniteness.groupInversion_intertwines line 107
  17. lemma OAI.WeakPureInfiniteness.inner_leftRight_regular_base line 113