OAI/Combinatorics/Chromatic/QuantumTorus/IndependentElementReindex.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.ElementaryPositivity.QuantumTorus.independent_mapline 14 - lemma
OAI.ElementaryPositivity.QuantumTorus.independentTerm_mapline 19 - lemma
OAI.ElementaryPositivity.QuantumTorus.independentElement_reindexline 25 - def
OAI.ElementaryPositivity.QuantumTorus.embeddingSumComplline 34 - lemma
OAI.ElementaryPositivity.QuantumTorus.embeddingSumCompl_inlline 37 - lemma
OAI.ElementaryPositivity.QuantumTorus.embeddingSumCompl_inrline 39