OAI/Combinatorics/Chromatic/Shuffle/FourTensorKernel.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ElementaryPositivity.RawShuffle.realize_inverseKernelUnit_unit line 33
  2. lemma OAI.ElementaryPositivity.RawShuffle.fourKernel_lift_naturality line 39
  3. lemma OAI.ElementaryPositivity.RawShuffle.fourKernel_restrictRows line 56
  4. lemma OAI.ElementaryPositivity.RawShuffle.fourKernel_firstColumn line 65
  5. lemma OAI.ElementaryPositivity.RawShuffle.fourKernel_secondColumn line 82
  6. lemma OAI.ElementaryPositivity.RawShuffle.fourKernel_crossingColumn line 99
  7. lemma OAI.ElementaryPositivity.RawShuffle.fourTensor_cross_realize line 112
  8. def OAI.ElementaryPositivity.RawShuffle.mappedInverseKernel line 137
  9. def OAI.ElementaryPositivity.RawShuffle.fourRowsInverseUnit line 152
  10. def OAI.ElementaryPositivity.RawShuffle.fourFirstInverseUnit line 156
  11. def OAI.ElementaryPositivity.RawShuffle.fourSecondInverseUnit line 160
  12. def OAI.ElementaryPositivity.RawShuffle.fourCrossingInverseUnit line 164
  13. lemma OAI.ElementaryPositivity.RawShuffle.fourTotalInverseUnit_zero line 168
  14. def OAI.ElementaryPositivity.RawShuffle.fourSeriesValue line 175
  15. lemma OAI.ElementaryPositivity.RawShuffle.fourSeriesValue_injective line 180
  16. lemma OAI.ElementaryPositivity.RawShuffle.fourSeriesValue_rows line 184
  17. lemma OAI.ElementaryPositivity.RawShuffle.fourSeriesValue_first line 189
  18. lemma OAI.ElementaryPositivity.RawShuffle.fourSeriesValue_second line 195
  19. lemma OAI.ElementaryPositivity.RawShuffle.fourSeriesValue_crossing line 201
  20. lemma OAI.ElementaryPositivity.RawShuffle.fourSeriesValue_cross line 207
  21. lemma OAI.ElementaryPositivity.RawShuffle.units_map_neg_one line 212
  22. lemma OAI.ElementaryPositivity.RawShuffle.ring_map_unit_val line 218
  23. lemma OAI.ElementaryPositivity.RawShuffle.ring_map_inv_unit_val line 221
  24. lemma OAI.ElementaryPositivity.RawShuffle.ring_map_signedUnits line 224
  25. lemma OAI.ElementaryPositivity.RawShuffle.unitKernelCancellation_lift line 232
  26. lemma OAI.ElementaryPositivity.RawShuffle.unitKernelCancellation_lift2 line 246
  27. lemma OAI.ElementaryPositivity.RawShuffle.fourSeriesValue_rows_val line 255
  28. lemma OAI.ElementaryPositivity.RawShuffle.fourSeriesValue_rows_inv_val line 261
  29. def OAI.ElementaryPositivity.RawShuffle.fourTensorKernelRHS line 267
  30. lemma OAI.ElementaryPositivity.RawShuffle.fourSeriesValue_kernelRHS line 274
  31. lemma OAI.ElementaryPositivity.RawShuffle.fourSeriesValue_kernelRHS_val line 292
  32. lemma OAI.ElementaryPositivity.RawShuffle.fourSeriesValue_kernelLHS line 298
  33. lemma OAI.ElementaryPositivity.RawShuffle.fourTensorKernel_cancellation line 310