OAI/Combinatorics/Chromatic/Shuffle/CanonicalCard.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.RawShuffle.canonical_source_card line 18
2. lemma OAI.ElementaryPositivity.RawShuffle.fourGridPolynomial_zero_of_source_mismatch line 30
3. lemma OAI.ElementaryPositivity.RawShuffle.quotient_gridShapeTensor_zero line 43
4. lemma OAI.ElementaryPositivity.RawShuffle.quotient_gridTensor_zero line 63
5. def OAI.ElementaryPositivity.RawShuffle.crossSign line 84
6. lemma OAI.ElementaryPositivity.RawShuffle.sameDen_realization line 88
7. lemma OAI.ElementaryPositivity.RawShuffle.targetEmbedding_crossDifference line 101
8. lemma OAI.ElementaryPositivity.RawShuffle.targetValueAt_crossTensor line 121
9. lemma OAI.ElementaryPositivity.RawShuffle.targetValueAt_smul line 138
10. lemma OAI.ElementaryPositivity.RawShuffle.cleared_restrictTensor line 144
11. def OAI.ElementaryPositivity.RawShuffle.relativeTaylorB line 162
12. lemma OAI.ElementaryPositivity.RawShuffle.relativeTaylorB_tmul line 170
13. lemma OAI.ElementaryPositivity.RawShuffle.quotientTensor_tmul line 178
14. lemma OAI.ElementaryPositivity.RawShuffle.relativeTaylor_quotient line 182
15. lemma OAI.ElementaryPositivity.RawShuffle.quotient_relativeTaylor_zero line 199
16. lemma OAI.ElementaryPositivity.RawShuffle.quotient_crossTensor_cancel line 204