OAI/Combinatorics/Chromatic/Walls/MutatedPathCompletion.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.QuantumTorus.mutatedPathProduct line 20
2. def OAI.ElementaryPositivity.QuantumTorus.mutatedPathCompletion line 27
3. lemma OAI.ElementaryPositivity.QuantumTorus.mutatedPathCompletion_coeff line 34
4. lemma OAI.ElementaryPositivity.QuantumTorus.mutatedPathCompletion_trans line 49
5. lemma OAI.ElementaryPositivity.QuantumTorus.mutatedPathCompletion_constant line 59
6. lemma OAI.ElementaryPositivity.QuantumTorus.mutatedPathCompletion_graded line 70
7. def OAI.ElementaryPositivity.QuantumTorus.mutatedPathCompletedPositive line 79
8. lemma OAI.ElementaryPositivity.QuantumTorus.mutationCompletion_list_prod line 99
9. def OAI.ElementaryPositivity.QuantumTorus.noncutOldLineFactor line 125
10. lemma OAI.ElementaryPositivity.QuantumTorus.cutSide_decision line 133
11. lemma OAI.ElementaryPositivity.QuantumTorus.mutatedLineFactor_nocut line 141
12. lemma OAI.ElementaryPositivity.QuantumTorus.noncutOldLineFactor_bound line 156
13. lemma OAI.ElementaryPositivity.QuantumTorus.noncutOldLineFactor_comparison line 175