OAI/Combinatorics/Chromatic/Shuffle/RenameFraction.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.ShufflePolynomiality.renameFraction line 13
2. lemma OAI.ElementaryPositivity.ShufflePolynomiality.renameFraction_algebraMap line 21
3. lemma OAI.ElementaryPositivity.ShufflePolynomiality.naturalVandermonde_ne_zero line 35
4. theorem OAI.ElementaryPositivity.ShufflePolynomiality.rational_pack_sum_polynomial line 43
5. def OAI.ElementaryPositivity.ShufflePolynomiality.crossDenominator line 86
6. lemma OAI.ElementaryPositivity.ShufflePolynomiality.crossDenominator_dvd line 94
7. theorem OAI.ElementaryPositivity.ShufflePolynomiality.shuffle_denominator_sum_polynomial line 99
8. lemma OAI.ElementaryPositivity.ShufflePolynomiality.packed_pairs_product_dvd line 117
9. lemma OAI.ElementaryPositivity.ShufflePolynomiality.diagonal_dvd_naturalVandermonde line 144
10. theorem OAI.ElementaryPositivity.ShufflePolynomiality.invariant_fraction_regular line 161