OAI/Combinatorics/Chromatic/Walls/RayIncomingIdentification.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.FormalLog.log_injective_through line 12
2. lemma OAI.ElementaryPositivity.FormalLog.log_injective line 26
3. def OAI.ElementaryPositivity.QuantumTorus.OnPositiveRay line 39
4. lemma OAI.ElementaryPositivity.QuantumTorus.OnPositiveRay.refl line 41
5. lemma OAI.ElementaryPositivity.QuantumTorus.OnPositiveRay.eval line 42
6. lemma OAI.ElementaryPositivity.QuantumTorus.OnPositiveRay.incomingSigns line 53
7. lemma OAI.ElementaryPositivity.QuantumTorus.chart_sign_congr line 62
8. lemma OAI.ElementaryPositivity.QuantumTorus.incoming_same_ray line 74
9. theorem OAI.ElementaryPositivity.QuantumTorus.incoming_ray_log line 78
10. lemma OAI.ElementaryPositivity.QuantumTorus.positive_ray_of_pairing_zero line 99
11. lemma OAI.ElementaryPositivity.QuantumTorus.finite_positive_ray_order line 111