OAI/Combinatorics/Chromatic/Walls/PowerSeriesThreeFactors.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.PowerSeriesSplit.positiveFactor line 17
2. def OAI.ElementaryPositivity.PowerSeriesSplit.zeroFactor line 18
3. def OAI.ElementaryPositivity.PowerSeriesSplit.negativeFactor line 19
4. lemma OAI.ElementaryPositivity.PowerSeriesSplit.factor_three line 21
5. lemma OAI.ElementaryPositivity.PowerSeriesSplit.zero_negative_nonpositive line 27
6. lemma OAI.ElementaryPositivity.PowerSeriesSplit.three_constant line 38
7. lemma OAI.ElementaryPositivity.PowerSeriesSplit.three_support line 44
8. lemma OAI.ElementaryPositivity.PowerSeriesSplit.three_uniqueness line 55