OAI/Combinatorics/Chromatic/Walls/LaurentPolynomialEnergy.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.LaurentPositive.qLaurent line 13
2. lemma OAI.ElementaryPositivity.LaurentPositive.qLaurent_monomial line 15
3. def OAI.ElementaryPositivity.LaurentPositive.centered line 22
4. lemma OAI.ElementaryPositivity.LaurentPositive.centered_zero line 23
5. lemma OAI.ElementaryPositivity.LaurentPositive.centered_add line 24
6. lemma OAI.ElementaryPositivity.LaurentPositive.centered_sum line 26
7. lemma OAI.ElementaryPositivity.LaurentPositive.centered_mul line 28
8. lemma OAI.ElementaryPositivity.LaurentPositive.centered_monomial line 30
9. lemma OAI.ElementaryPositivity.LaurentPositive.centered_coeff line 34
10. lemma OAI.ElementaryPositivity.LaurentPositive.centered_injective line 43
11. lemma OAI.ElementaryPositivity.LaurentPositive.centered_X_pow line 49
12. lemma OAI.ElementaryPositivity.LaurentPositive.map_elementary_coeff line 55