OAI/Combinatorics/Chromatic/Walls/MutationIncomingFinite.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.QuantumTorus.literalIncomingRay_eq_one_of_none line 13
2. lemma OAI.ElementaryPositivity.QuantumTorus.literalIncoming_simple_nonsimple line 23
3. lemma OAI.ElementaryPositivity.QuantumTorus.nonsimple_incoming_at_far_through line 36
4. lemma OAI.ElementaryPositivity.QuantumTorus.pushed_nonsimple_incoming_at_far line 49
5. lemma OAI.ElementaryPositivity.QuantumTorus.mutationIncomingLabel_nsmul line 68
6. lemma OAI.ElementaryPositivity.QuantumTorus.mutationIncomingLabel_positive_ray_iff line 81
7. lemma OAI.ElementaryPositivity.QuantumTorus.mutationIncomingLabel_simple line 94
8. lemma OAI.ElementaryPositivity.QuantumTorus.mutationIncomingLabel_simple_ray_iff line 98