OAI/Combinatorics/Chromatic/Shuffle/CellLeadingSum.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.RawShuffle.cellLeadingB line 18
2. lemma OAI.ElementaryPositivity.RawShuffle.clearedConstantB_cell_leading line 32
3. def OAI.ElementaryPositivity.RawShuffle.castBTensor line 60
4. lemma OAI.ElementaryPositivity.RawShuffle.castBTensor_sub line 67
5. lemma OAI.ElementaryPositivity.RawShuffle.clearedConstantB_castTensor line 75
6. lemma OAI.ElementaryPositivity.RawShuffle.castBTensor_mem_unitalSource line 83
7. def OAI.ElementaryPositivity.RawShuffle.gridShapeLeadingB line 93
8. lemma OAI.ElementaryPositivity.RawShuffle.clearedConstantB_gridShape_leading line 104
9. def OAI.ElementaryPositivity.RawShuffle.gridLeadingB line 125
10. lemma OAI.ElementaryPositivity.RawShuffle.clearedConstantB_grid_leading line 135
11. lemma OAI.ElementaryPositivity.RawShuffle.unitalSeparationConstant_shuffle_leading line 158