OAI/Combinatorics/Chromatic/Walls/SectionRayTransition.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.QuantumTorus.section_ray_positive_side line 14
2. lemma OAI.ElementaryPositivity.QuantumTorus.section_ray_negative_side line 29
3. lemma OAI.ElementaryPositivity.QuantumTorus.section_ray_crossing line 42
4. def OAI.ElementaryPositivity.QuantumTorus.ChamberGeneric line 71
5. lemma OAI.ElementaryPositivity.QuantumTorus.realRoot_ne_zero line 74
6. lemma OAI.ElementaryPositivity.QuantumTorus.realRoot_exists line 81
7. lemma OAI.ElementaryPositivity.QuantumTorus.section_event_ray line 89
8. lemma OAI.ElementaryPositivity.QuantumTorus.section_offset_generic line 116
9. lemma OAI.ElementaryPositivity.QuantumTorus.section_line_zero_not_event line 122
10. lemma OAI.ElementaryPositivity.QuantumTorus.line_covector_add line 131
11. lemma OAI.ElementaryPositivity.QuantumTorus.line_covector_sub line 137