OAI/Combinatorics/Chromatic/Shuffle/TensorSymbolSwap.lean
10 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.ElementaryPositivity.RawShuffle.SplitTree.box_swapline 15 - def
OAI.ElementaryPositivity.RawShuffle.SplitTree.sourceTensorCommline 27 - lemma
OAI.ElementaryPositivity.RawShuffle.SplitTree.normalizedTensorSymbol_tmul_eqline 32 - lemma
OAI.ElementaryPositivity.RawShuffle.SplitTree.normalizedTensorSymbol_swapline 44 - def
OAI.ElementaryPositivity.RawShuffle.sourceGradeDimensionEquivline 93 - lemma
OAI.ElementaryPositivity.RawShuffle.sourceGradeDimensionEquiv_mkline 99 - def
OAI.ElementaryPositivity.RawShuffle.sourceTensorGradeCommline 106 - lemma
OAI.ElementaryPositivity.RawShuffle.sourceTensorGradeComm_mkline 111 - lemma
OAI.ElementaryPositivity.RawShuffle.separationCoproduct_mkline 116 - theorem
OAI.ElementaryPositivity.RawShuffle.separationCoproduct_cocommutativeline 123