OAI/Analysis/OInfinity/EvenRowCAR.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

The CAR seed of a finite even Cuntz row

The given row is indexed by Fin 2 × Fin n. Its two equal blocks supply matrix units with corner unit q, even when the row has more than two members. The resulting seed commutes with the actual row shift.

  1. def OAI.WeakPureInfiniteness.evenRowMatrixUnit line 19
  2. def OAI.WeakPureInfiniteness.evenRowShift line 22
  3. def OAI.WeakPureInfiniteness.evenRowSeed line 25
  4. def OAI.WeakPureInfiniteness.evenRowParity line 27
  5. def OAI.WeakPureInfiniteness.evenRowCAR line 30
  6. lemma OAI.WeakPureInfiniteness.evenRowMatrixUnit_star line 34
  7. lemma OAI.WeakPureInfiniteness.evenRowShift_star line 38
  8. lemma OAI.WeakPureInfiniteness.evenRowShift_add line 42
  9. lemma OAI.WeakPureInfiniteness.evenRowShift_zero line 46
  10. lemma OAI.WeakPureInfiniteness.evenRow_right_support line 56
  11. lemma OAI.WeakPureInfiniteness.evenRow_left_support line 61
  12. lemma OAI.WeakPureInfiniteness.evenRowMatrixUnit_mul line 73
  13. lemma OAI.WeakPureInfiniteness.evenRowMatrixUnit_sum line 94
  14. lemma OAI.WeakPureInfiniteness.evenRowMatrixUnit_support line 98
  15. lemma OAI.WeakPureInfiniteness.evenRowSeed_relations line 110
  16. lemma OAI.WeakPureInfiniteness.evenRowParity_relations line 126
  17. lemma OAI.WeakPureInfiniteness.evenRowMatrixUnit_mul_row line 145
  18. lemma OAI.WeakPureInfiniteness.evenRow_star_row_mul_MatrixUnit line 161
  19. lemma OAI.WeakPureInfiniteness.evenRowMatrixUnit_commute_shift line 172
  20. lemma OAI.WeakPureInfiniteness.evenRowSeed_commute_shift line 204
  21. lemma OAI.WeakPureInfiniteness.evenRowParity_commute_shift line 208
  22. lemma OAI.WeakPureInfiniteness.evenRowShift_support line 213
  23. lemma OAI.WeakPureInfiniteness.evenRowShift_unit line 224
  24. lemma OAI.WeakPureInfiniteness.evenRowShift_mul line 228
  25. lemma OAI.WeakPureInfiniteness.evenRowCAR_support line 245