OAI/Combinatorics/Chromatic/Walls/DegreeIsolatedReordering.lean
10 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.ElementaryPositivity.RootTruncation.patchTopline 12 - lemma
OAI.ElementaryPositivity.RootTruncation.coeff_patchTopline 14 - lemma
OAI.ElementaryPositivity.RootTruncation.patchTop_lowline 17 - lemma
OAI.ElementaryPositivity.RootTruncation.patchTop_lastline 19 - lemma
OAI.ElementaryPositivity.RootTruncation.patchTop_constantline 21 - lemma
OAI.ElementaryPositivity.QuantumTorus.SeriesConverges.zero_middleline 31 - lemma
OAI.ElementaryPositivity.QuantumTorus.SeriesGraded.patchTopline 42 - lemma
OAI.ElementaryPositivity.QuantumTorus.SeriesConverges.patchTopline 51 - lemma
OAI.ElementaryPositivity.QuantumTorus.zero_middle_offline 65 - lemma
OAI.ElementaryPositivity.QuantumTorus.joint_middle_isolated_throughline 71