OAI/Combinatorics/Chromatic/Walls/LaurentFiniteDecorations.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.LaurentPositive.multiplicity line 13
2. lemma OAI.ElementaryPositivity.LaurentPositive.multiplicity_cast line 14
3. lemma OAI.ElementaryPositivity.LaurentPositive.coeff_nonneg line 16
4. lemma OAI.ElementaryPositivity.LaurentPositive.coeff_mul_natCast line 20
5. lemma OAI.ElementaryPositivity.LaurentPositive.support_of_positive_sum line 27
6. lemma OAI.ElementaryPositivity.LaurentPositive.exponent_injective line 44
7. lemma OAI.ElementaryPositivity.LaurentPositive.finite_expansion line 50
8. abbrev OAI.ElementaryPositivity.LaurentPositive.Decoration line 74
9. lemma OAI.ElementaryPositivity.LaurentPositive.decoration_expansion line 77