OAI/Combinatorics/Chromatic/Shuffle/SignedCoproductGridGrade.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.LinearFiltration.mk_eq_mk_iff_sub_mem line 11
2. lemma OAI.ElementaryPositivity.RawShuffle.unitalSourceTensorFiltration_antitone line 25
3. lemma OAI.ElementaryPositivity.RawShuffle.gridLeadingB_mem line 30
4. def OAI.ElementaryPositivity.RawShuffle.gridLeadingGrade line 53
5. lemma OAI.ElementaryPositivity.RawShuffle.unitalGradeCoproduct_shuffle_grid line 64
6. def OAI.ElementaryPositivity.RawShuffle.cutShapeDimensionEquiv line 96
7. lemma OAI.ElementaryPositivity.RawShuffle.cutShapeDimensionEquiv_left line 101
8. lemma OAI.ElementaryPositivity.RawShuffle.cutShapeDimensionEquiv_right line 106
9. lemma OAI.ElementaryPositivity.RawShuffle.sum_cutShapeDimensionEquiv line 114
10. def OAI.ElementaryPositivity.RawShuffle.dimensionRowLeadingB line 130
11. def OAI.ElementaryPositivity.RawShuffle.dimensionLeadingB line 138
12. lemma OAI.ElementaryPositivity.RawShuffle.cast_cellLeadingB_congr line 142
13. lemma OAI.ElementaryPositivity.RawShuffle.gridLeadingB_eq_dimensionLeadingB line 156