OAI/Combinatorics/Chromatic/Walls/IncomingRayElement.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.QuantumTorus.root_graded_log line 15
2. lemma OAI.ElementaryPositivity.QuantumTorus.OnPositiveRay.add line 23
3. lemma OAI.ElementaryPositivity.QuantumTorus.incoming_ray_log_support line 35
4. theorem OAI.ElementaryPositivity.QuantumTorus.incoming_ray_element_through line 59
5. lemma OAI.ElementaryPositivity.QuantumTorus.incoming_unique_through line 101
6. lemma OAI.ElementaryPositivity.QuantumTorus.completed_list_constant line 127
7. lemma OAI.ElementaryPositivity.QuantumTorus.completed_list_graded line 133
8. def OAI.ElementaryPositivity.QuantumTorus.completedListProduct line 141
9. lemma OAI.ElementaryPositivity.QuantumTorus.completed_list_supported line 145
10. lemma OAI.ElementaryPositivity.QuantumTorus.incoming_coefficient_supported line 159
11. lemma OAI.ElementaryPositivity.QuantumTorus.strict_list_product_through line 172
12. lemma OAI.ElementaryPositivity.QuantumTorus.ordered_ray_middle line 184
13. theorem OAI.ElementaryPositivity.QuantumTorus.joint_recovered_from_incoming line 231