OAI/Combinatorics/Chromatic/QuantumTorus/SectionCharts.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.ElementaryPositivity.QuantumTorus.negative_sign_congr_throughline 14 - lemma
OAI.ElementaryPositivity.QuantumTorus.section_sign_congr_throughline 27 - lemma
OAI.ElementaryPositivity.QuantumTorus.section_refinement_throughline 35 - lemma
OAI.ElementaryPositivity.QuantumTorus.section_incoming_perturbationline 47 - lemma
OAI.ElementaryPositivity.QuantumTorus.chartNegative_of_positive_throughline 63 - lemma
OAI.ElementaryPositivity.QuantumTorus.chartNegative_of_negative_throughline 69