OAI/Analysis/WeakInfiniteness/SupportedCorner.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakPureInfiniteness.supportedAlgebra line 25
  2. lemma OAI.WeakPureInfiniteness.supportedAlgebra_closed line 43
  3. instance OAI.WeakPureInfiniteness.supportedAlgebra_complete line 47
  4. def OAI.WeakPureInfiniteness.matrixSingletonHom line 50
  5. lemma OAI.WeakPureInfiniteness.matrixSingletonHom_injective line 60
  6. lemma OAI.WeakPureInfiniteness.rectangular_mul_zero_support line 70
  7. lemma OAI.WeakPureInfiniteness.rectangular_zero_mul_support line 73
  8. lemma OAI.WeakPureInfiniteness.rectangular_mul_add_support line 76
  9. lemma OAI.WeakPureInfiniteness.rectangular_add_mul_support line 79
  10. lemma OAI.WeakPureInfiniteness.rectangular_mul_smul_support line 82
  11. lemma OAI.WeakPureInfiniteness.rectangular_smul_mul_support line 85
  12. def OAI.WeakPureInfiniteness.supportedCompression line 90
  13. lemma OAI.WeakPureInfiniteness.supportedCompression_inverse line 111
  14. lemma OAI.WeakPureInfiniteness.supportedCompression_injective line 119