OAI/Combinatorics/Chromatic/GradedAlgebra/EnergyLaurentFinite.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.ElementaryPositivity.EnergyLaurent.admissible_subtypeline 11 - def
OAI.ElementaryPositivity.EnergyLaurent.sigmaEnergyFiberline 24 - lemma
OAI.ElementaryPositivity.EnergyLaurent.admissible_sigmaline 31 - lemma
OAI.ElementaryPositivity.EnergyLaurent.series_sigmaline 43