OAI/Combinatorics/Chromatic/Shuffle/GlobalTensorInduction.lean
12 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.ElementaryPositivity.RawShuffle.globalTensor_inductionline 13 - lemma
OAI.ElementaryPositivity.RawShuffle.globalLof_mulline 34 - lemma
OAI.ElementaryPositivity.RawShuffle.euler_interchange_cocycleline 53 - lemma
OAI.ElementaryPositivity.RawShuffle.globalSignedTensorMultiply_assoc_homogeneousline 60 - lemma
OAI.ElementaryPositivity.RawShuffle.globalSignedTensorMultiply_assocline 90 - lemma
OAI.ElementaryPositivity.RawShuffle.globalSignedTensorMultiply_one_leftline 117 - lemma
OAI.ElementaryPositivity.RawShuffle.globalSignedTensorMultiply_one_rightline 131 - def
OAI.ElementaryPositivity.RawShuffle.SignedGlobalTensorline 145 - instance
OAI.ElementaryPositivity.RawShuffle.(instance at line 149)line 149 - instance
OAI.ElementaryPositivity.RawShuffle.(instance at line 152)line 152 - instance
OAI.ElementaryPositivity.RawShuffle.(instance at line 155)line 155 - instance
OAI.ElementaryPositivity.RawShuffle.(instance at line 178)line 178