OAI/Combinatorics/Chromatic/Shuffle/DimensionColumnLeading.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.RawShuffle.sum_subtype_of_zero_off line 14
2. lemma OAI.ElementaryPositivity.RawShuffle.dimensionRowLeadingB_zero_of_mismatch line 24
3. def OAI.ElementaryPositivity.RawShuffle.dimensionColumnLeadingB line 35
4. lemma OAI.ElementaryPositivity.RawShuffle.dimensionColumnLeadingB_transpose line 44
5. lemma OAI.ElementaryPositivity.RawShuffle.double_sum_eq_column_grid line 63
6. theorem OAI.ElementaryPositivity.RawShuffle.dimensionLeadingB_eq_column_sum line 76
7. lemma OAI.ElementaryPositivity.RawShuffle.clearedConstantB_grid_unital_support line 99
8. lemma OAI.ElementaryPositivity.RawShuffle.clearedConstantB_grid_leading_unital line 115
9. lemma OAI.ElementaryPositivity.RawShuffle.unitalSeparationConstant_shuffle_leading_all line 139
10. theorem OAI.ElementaryPositivity.RawShuffle.unitalSeparationConstant_shuffle_column line 155