OAI/Combinatorics/Chromatic/GradedAlgebra/EnergyLaurentSeries.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.EnergyLaurent.Admissible line 12
2. def OAI.ElementaryPositivity.EnergyLaurent.family line 15
3. def OAI.ElementaryPositivity.EnergyLaurent.series line 36
4. lemma OAI.ElementaryPositivity.EnergyLaurent.series_coeff line 38
5. lemma OAI.ElementaryPositivity.EnergyLaurent.series_eq_of_cards line 60
6. lemma OAI.ElementaryPositivity.EnergyLaurent.admissible_prod line 66
7. lemma OAI.ElementaryPositivity.EnergyLaurent.series_mul line 85
8. lemma OAI.ElementaryPositivity.EnergyLaurent.admissible_of_cards line 96
9. lemma OAI.ElementaryPositivity.EnergyLaurent.admissible_shift line 109
10. lemma OAI.ElementaryPositivity.EnergyLaurent.series_shift line 121
11. lemma OAI.ElementaryPositivity.EnergyLaurent.series_equiv line 132
12. lemma OAI.ElementaryPositivity.EnergyLaurent.admissible_sum line 138
13. lemma OAI.ElementaryPositivity.EnergyLaurent.series_sum line 153