OAI/Analysis/WeakInfiniteness/MatrixTensorExact.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakPureInfiniteness.matrixEntryLinear line 33
  2. def OAI.WeakPureInfiniteness.matrixUnit line 38
  3. lemma OAI.WeakPureInfiniteness.matrix_unit_expansion line 41
  4. def OAI.WeakPureInfiniteness.matrixEntryContinuous line 49
  5. def OAI.WeakPureInfiniteness.matrixTensorReconstruct line 54
  6. lemma OAI.WeakPureInfiniteness.matrixTensorReconstruct_apply line 57
  7. lemma OAI.WeakPureInfiniteness.minimalElementary_balance line 62
  8. lemma OAI.WeakPureInfiniteness.matrixTensorReconstruct_coefficient line 67
  9. lemma OAI.WeakPureInfiniteness.matrixTensorReconstruct_coordinates line 75
  10. lemma OAI.WeakPureInfiniteness.matrixTensorCoordinates_right_comm line 85
  11. lemma OAI.WeakPureInfiniteness.matrixTensor_kernel line 103