OAI/Combinatorics/Chromatic/Shuffle/GridShapeFiltration.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.RawShuffle.ShuffleFiltered line 15
2. lemma OAI.ElementaryPositivity.RawShuffle.quotient_fourGrid_filtered line 23
3. lemma OAI.ElementaryPositivity.RawShuffle.quotientTensor_cast_mem_unitalSource line 49
4. lemma OAI.ElementaryPositivity.RawShuffle.quotient_gridShapeTensor_filtered line 60
5. lemma OAI.ElementaryPositivity.RawShuffle.restriction_shuffleBUnit_filtered line 92
6. lemma OAI.ElementaryPositivity.RawShuffle.sourceFiltration_of_binary line 138