OAI/Analysis/WeakInfiniteness/CrossUniverseTensorMap.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WeakPureInfiniteness.minimalElementary_mul line 35
  2. lemma OAI.WeakPureInfiniteness.minimalElementary_star line 39
  3. lemma OAI.WeakPureInfiniteness.minimalElementary_smul_left line 43
  4. def OAI.WeakPureInfiniteness.crossTensorPair line 49
  5. lemma OAI.WeakPureInfiniteness.crossTensorPair_mul line 52
  6. lemma OAI.WeakPureInfiniteness.crossTensorPair_star line 56
  7. def OAI.WeakPureInfiniteness.crossTensorGraph line 59
  8. instance OAI.WeakPureInfiniteness.crossTensorGraphCStar line 62
  9. lemma OAI.WeakPureInfiniteness.crossTensorGraph_norm line 66
  10. def OAI.WeakPureInfiniteness.crossTensorFirst line 88
  11. def OAI.WeakPureInfiniteness.crossTensorSecond line 96
  12. lemma OAI.WeakPureInfiniteness.crossTensorFirst_isometry line 104
  13. lemma OAI.WeakPureInfiniteness.crossTensorFirst_surjective line 110
  14. def OAI.WeakPureInfiniteness.minimalMapAny line 123
  15. lemma OAI.WeakPureInfiniteness.minimalMapAny_elementary line 128