OAI/Combinatorics/Chromatic/Shuffle/TensorMiddleEnd.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.middleGroup line 15
  2. lemma OAI.ElementaryPositivity.middleGroup_tmul line 19
  3. lemma OAI.ElementaryPositivity.middleGroup_symm_tmul line 22
  4. def OAI.ElementaryPositivity.middleEnd line 25
  5. lemma OAI.ElementaryPositivity.middleEnd_scalar line 31
  6. def OAI.ElementaryPositivity.RawShuffle.globalSignOperator line 50
  7. lemma OAI.ElementaryPositivity.RawShuffle.globalSignOperator_tmul_lof line 60
  8. def OAI.ElementaryPositivity.RawShuffle.globalSignedTensorMultiply line 72
  9. lemma OAI.ElementaryPositivity.RawShuffle.globalSignedTensorMultiply_tmul_lof line 81
  10. lemma OAI.ElementaryPositivity.RawShuffle.signedCellMultiplyB_tmul line 113
  11. lemma OAI.ElementaryPositivity.RawShuffle.mk_eq_smul_of_val_eq line 123
  12. lemma OAI.ElementaryPositivity.RawShuffle.signedCellGradeMultiply_part line 128