OAI/Analysis/WeakInfiniteness/MatrixTensorCoordinates.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakPureInfiniteness.scalarMatrixRep line 32
  2. lemma OAI.WeakPureInfiniteness.scalarMatrixRep_basis line 37
  3. def OAI.WeakPureInfiniteness.matrixTensorCoefficient line 45
  4. lemma OAI.WeakPureInfiniteness.matrixTensorCoefficient_eq line 49
  5. lemma OAI.WeakPureInfiniteness.norm_matrixTensorSum_le line 55
  6. def OAI.WeakPureInfiniteness.matrixTensorPolynomial line 69
  7. lemma OAI.WeakPureInfiniteness.norm_matrixTensorPolynomial_le line 72
  8. def OAI.WeakPureInfiniteness.matrixTensorCoordinates line 89
  9. lemma OAI.WeakPureInfiniteness.matrixTensorCoordinates_polynomial line 92
  10. lemma OAI.WeakPureInfiniteness.matrixTensorCoordinates_elementary line 97