OAI/Combinatorics/EuclideanRamsey/TensorPresentation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.EuclideanRamsey.AffineVector line 30
  2. def OAI.EuclideanRamsey.affineArray line 32
  3. lemma OAI.EuclideanRamsey.affineArray_tmul line 37
  4. def OAI.EuclideanRamsey.rowEvaluation line 41
  5. lemma OAI.EuclideanRamsey.arrayEvaluation_affineArray line 47
  6. lemma OAI.EuclideanRamsey.spatialMultiply_affineArray line 59
  7. lemma OAI.EuclideanRamsey.affineArray_comm line 70
  8. lemma OAI.EuclideanRamsey.arrayEvaluation_comm line 76
  9. lemma OAI.EuclideanRamsey.spatialMultiply_comm line 85
  10. theorem OAI.EuclideanRamsey.exists_symmetric_tensor_presentation line 102
  11. lemma OAI.EuclideanRamsey.rational_lattice_kernel line 149
  12. lemma OAI.EuclideanRamsey.quotientTensor_zero_of_evaluation line 176
  13. lemma OAI.EuclideanRamsey.matrixTensor_map_family line 200
  14. lemma OAI.EuclideanRamsey.spatialMultiply_family line 206
  15. theorem OAI.EuclideanRamsey.realCriterion_lattice line 224