OAI/Combinatorics/Chromatic/Walls/MutationChamberPaths.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.QuantumTorus.mutationSignRegion line 16
2. lemma OAI.ElementaryPositivity.QuantumTorus.cut_positive_intermediate line 21
3. lemma OAI.ElementaryPositivity.QuantumTorus.generic_mutation_region_path line 46
4. lemma OAI.ElementaryPositivity.QuantumTorus.mutatedLineFactor_protected line 142
5. lemma OAI.ElementaryPositivity.QuantumTorus.mutatedLineProduct_protected line 165
6. lemma OAI.ElementaryPositivity.QuantumTorus.mutatedPathCompletion_protected line 188
7. lemma OAI.ElementaryPositivity.QuantumTorus.mutatedTransport_protected line 224