OAI/Combinatorics/Chromatic/Walls/SimpleIncomingData.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.QuantumTorus.simpleDatum line 15
2. def OAI.ElementaryPositivity.QuantumTorus.simpleIncomingList line 16
3. lemma OAI.ElementaryPositivity.QuantumTorus.simpleDatum_allowed line 17
4. lemma OAI.ElementaryPositivity.QuantumTorus.simpleIncomingList_allowed line 19
5. def OAI.ElementaryPositivity.QuantumTorus.simpleTotalTransport line 24
6. lemma OAI.ElementaryPositivity.QuantumTorus.simpleTotalTransport_positive_prescription line 25
7. lemma OAI.ElementaryPositivity.QuantumTorus.simpleRoot_coordinates line 31
8. lemma OAI.ElementaryPositivity.QuantumTorus.nonpDegree_simple_self line 34
9. lemma OAI.ElementaryPositivity.QuantumTorus.simple_off_fiber line 41
10. lemma OAI.ElementaryPositivity.QuantumTorus.positive_nonp_not_simple_ray line 56
11. lemma OAI.ElementaryPositivity.QuantumTorus.simpleIncomingRay_fiber line 66
12. lemma OAI.ElementaryPositivity.QuantumTorus.simpleIncomingCompleted_fiber line 78
13. lemma OAI.ElementaryPositivity.QuantumTorus.literalTotalTransport_ray_prescription line 93