OAI/Combinatorics/Chromatic/Walls/GlobalWallPositive.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.QuantumTorus.PositiveIncomingPrescription line 14
2. lemma OAI.ElementaryPositivity.QuantumTorus.literalRootProducts_one line 21
3. theorem OAI.ElementaryPositivity.QuantumTorus.positive_walls_through line 30
4. def OAI.ElementaryPositivity.QuantumTorus.literalIncomingRay line 103
5. lemma OAI.ElementaryPositivity.QuantumTorus.literalIncomingRay_mem line 107
6. lemma OAI.ElementaryPositivity.QuantumTorus.literalIncomingRay_eq line 115
7. def OAI.ElementaryPositivity.QuantumTorus.literalIncomingCompleted line 120
8. def OAI.ElementaryPositivity.QuantumTorus.literalIncomingLog line 126
9. lemma OAI.ElementaryPositivity.QuantumTorus.literalIncomingLog_apply line 131
10. lemma OAI.ElementaryPositivity.QuantumTorus.literalIncomingLog_graded line 136
11. def OAI.ElementaryPositivity.QuantumTorus.literalTotalTransport line 142
12. lemma OAI.ElementaryPositivity.QuantumTorus.literalTotalTransport_prescription line 146