OAI/Combinatorics/Chromatic/QuantumTorus/MutationFiberArithmetic.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.ElementaryPositivity.QuantumTorus.mutationPairingline 13 - lemma
OAI.ElementaryPositivity.QuantumTorus.root_simple_expansionline 15 - lemma
OAI.ElementaryPositivity.QuantumTorus.root_pairing_coordinatesline 31 - lemma
OAI.ElementaryPositivity.QuantumTorus.max_zero_negline 43 - lemma
OAI.ElementaryPositivity.QuantumTorus.fiberUpper_flipline 47 - lemma
OAI.ElementaryPositivity.QuantumTorus.fiberUpper_simpleline 60 - lemma
OAI.ElementaryPositivity.QuantumTorus.fiber_shift_boundline 67