OAI/Combinatorics/Chromatic/Walls/RationalTensorDetection.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ElementaryPositivity.LinearDetection.basisLeft_natural line 13
  2. lemma OAI.ElementaryPositivity.LinearDetection.basisRight_natural line 22
  3. theorem OAI.ElementaryPositivity.LinearDetection.tensor_right_detect line 31
  4. theorem OAI.ElementaryPositivity.LinearDetection.tensor_left_detect line 45
  5. theorem OAI.ElementaryPositivity.LinearDetection.tensor_detect line 59
  6. theorem OAI.ElementaryPositivity.LinearDetection.tensor_map_zero_of_test_kernels line 79
  7. def OAI.ElementaryPositivity.LinearDetection.retract line 132
  8. lemma OAI.ElementaryPositivity.LinearDetection.retract_mem line 135
  9. lemma OAI.ElementaryPositivity.LinearDetection.retract_eq_self line 138
  10. lemma OAI.ElementaryPositivity.LinearDetection.retract_top line 141
  11. def OAI.ElementaryPositivity.LinearDetection.filtrationPiece line 145
  12. lemma OAI.ElementaryPositivity.LinearDetection.filtrationPiece_mem line 149
  13. lemma OAI.ElementaryPositivity.LinearDetection.filtrationPiece_kernel line 158
  14. lemma OAI.ElementaryPositivity.LinearDetection.filtrationPiece_sum line 166
  15. lemma OAI.ElementaryPositivity.LinearDetection.tensor_map_sum_left line 179
  16. lemma OAI.ElementaryPositivity.LinearDetection.tensor_map_sum_right line 187
  17. lemma OAI.ElementaryPositivity.LinearDetection.tensor_sum_pieces line 195
  18. def OAI.ElementaryPositivity.LinearDetection.testFiltration line 209
  19. lemma OAI.ElementaryPositivity.LinearDetection.mem_testFiltration line 214
  20. lemma OAI.ElementaryPositivity.LinearDetection.testFiltration_antitone line 220
  21. def OAI.ElementaryPositivity.LinearDetection.additiveTensorFiltration line 227
  22. lemma OAI.ElementaryPositivity.LinearDetection.tmul_mem_additiveTensorFiltration line 231
  23. lemma OAI.ElementaryPositivity.LinearDetection.map_mem_additiveTensorFiltration line 237
  24. theorem OAI.ElementaryPositivity.LinearDetection.additiveTensorFiltration_iff_tests line 248