OAI/Combinatorics/Chromatic/Walls/MutatedNoCutTransport.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.QuantumTorus.mutatedLineProduct_nocut_eq line 24
2. lemma OAI.ElementaryPositivity.QuantumTorus.mutatedLineCompletion_nocut line 70
3. lemma OAI.ElementaryPositivity.QuantumTorus.noncutComparisonWord_bound line 121
4. lemma OAI.ElementaryPositivity.QuantumTorus.noncutEndpointRatio_bound line 149
5. def OAI.ElementaryPositivity.QuantumTorus.negativeCovectorUnit line 174
6. def OAI.ElementaryPositivity.QuantumTorus.GenericLinePath.OnCutSide line 177
7. lemma OAI.ElementaryPositivity.QuantumTorus.mutatedPathCompletion_nocut line 185
8. theorem OAI.ElementaryPositivity.QuantumTorus.mutatedPathCompletion_nocut_independent line 225