OAI/Combinatorics/Chromatic/QuantumTorus/StringStripDimension.lean
10 declarations, 0 contain sorry, 0 declared as axioms
- abbrev
OAI.ElementaryPositivity.UnitSelections.StringCountsline 14 - abbrev
OAI.ElementaryPositivity.UnitSelections.StripCountsline 16 - def
OAI.ElementaryPositivity.UnitSelections.stringStripDimensionEquivline 19 - def
OAI.ElementaryPositivity.UnitSelections.stringEnergyline 26 - def
OAI.ElementaryPositivity.UnitSelections.stripEnergyline 29 - lemma
OAI.ElementaryPositivity.UnitSelections.stringStripDimension_energyline 32 - lemma
OAI.ElementaryPositivity.UnitSelections.stringEnergy_shiftline 40 - def
OAI.ElementaryPositivity.UnitSelections.stripInsertline 54 - lemma
OAI.ElementaryPositivity.UnitSelections.stripInsert_injectiveline 61 - lemma
OAI.ElementaryPositivity.UnitSelections.stripInsert_energyline 67