OAI/Combinatorics/Chromatic/Walls/WeightedRay.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.ElementaryPositivity.QuantumTorus.weightedRayline 16 - lemma
OAI.ElementaryPositivity.QuantumTorus.coeff_weightedRayline 19 - lemma
OAI.ElementaryPositivity.QuantumTorus.weightedRay_oneline 24 - lemma
OAI.ElementaryPositivity.QuantumTorus.weightedRay_mulline 28 - lemma
OAI.ElementaryPositivity.QuantumTorus.weightedRay_twistline 33 - lemma
OAI.ElementaryPositivity.WeightedTorusSeries.weight_posline 51 - lemma
OAI.ElementaryPositivity.WeightedTorusSeries.push_on_rayline 59