OAI/Combinatorics/Chromatic/Walls/ShuffleTensorLinear.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.RawShuffle.shuffleTensorLinear line 13
2. lemma OAI.ElementaryPositivity.RawShuffle.shuffleTensorLinear_tmul line 16
3. lemma OAI.ElementaryPositivity.RawShuffle.tensorShuffle_tensorValue line 19
4. lemma OAI.ElementaryPositivity.RawShuffle.invariant_transfer_eq line 27
5. lemma OAI.ElementaryPositivity.RawShuffle.shuffleTensorLinear_mem line 34
6. def OAI.ElementaryPositivity.RawShuffle.twoTargetTransfer line 40
7. lemma OAI.ElementaryPositivity.RawShuffle.twoTargetTransfer_tmul line 45
8. lemma OAI.ElementaryPositivity.RawShuffle.shuffleImage_le_destabilizing line 51
9. lemma OAI.ElementaryPositivity.RawShuffle.quotient_shuffleTensorLinear_zero line 58
10. lemma OAI.ElementaryPositivity.RawShuffle.quotient_twoTargetTransfer_zero line 64