OAI/Combinatorics/Chromatic/Shuffle/GlobalTensorInduction.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ElementaryPositivity.RawShuffle.globalTensor_induction line 13
  2. lemma OAI.ElementaryPositivity.RawShuffle.globalLof_mul line 34
  3. lemma OAI.ElementaryPositivity.RawShuffle.euler_interchange_cocycle line 53
  4. lemma OAI.ElementaryPositivity.RawShuffle.globalSignedTensorMultiply_assoc_homogeneous line 60
  5. lemma OAI.ElementaryPositivity.RawShuffle.globalSignedTensorMultiply_assoc line 90
  6. lemma OAI.ElementaryPositivity.RawShuffle.globalSignedTensorMultiply_one_left line 117
  7. lemma OAI.ElementaryPositivity.RawShuffle.globalSignedTensorMultiply_one_right line 131
  8. def OAI.ElementaryPositivity.RawShuffle.SignedGlobalTensor line 145
  9. instance OAI.ElementaryPositivity.RawShuffle.(instance at line 149) line 149
  10. instance OAI.ElementaryPositivity.RawShuffle.(instance at line 152) line 152
  11. instance OAI.ElementaryPositivity.RawShuffle.(instance at line 155) line 155
  12. instance OAI.ElementaryPositivity.RawShuffle.(instance at line 178) line 178