OAI/Combinatorics/Chromatic/Shuffle/TensorFiltration.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.ElementaryPositivity.RawShuffle.RestrictionIndex line 15
2. def OAI.ElementaryPositivity.RawShuffle.RestrictionIndex.weight line 23
3. def OAI.ElementaryPositivity.RawShuffle.indexedRestriction line 27
4. lemma OAI.ElementaryPositivity.RawShuffle.sourceFiltration_eq_testFiltration line 31
5. def OAI.ElementaryPositivity.RawShuffle.sourceTensorFiltration line 43
6. theorem OAI.ElementaryPositivity.RawShuffle.sourceTensorFiltration_iff line 48
7. theorem OAI.ElementaryPositivity.RawShuffle.tensor_leading_restrictions_detect line 68
8. lemma OAI.ElementaryPositivity.IndependentCoefficientTensor.sumElim_eq_iff line 90
9. lemma OAI.ElementaryPositivity.IndependentCoefficientTensor.coeff_independent_product line 99
10. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.centerTranslation_node_coeff line 125
11. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.restrictionTest_node line 148
12. lemma OAI.ElementaryPositivity.RawShuffle.restrictionB_sourceTensorFiltration line 168