OAI/Combinatorics/Chromatic/Walls/SimpleAdjointFiber.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.QuantumTorus.simpleOriented line 20
2. def OAI.ElementaryPositivity.QuantumTorus.sideSign line 23
3. lemma OAI.ElementaryPositivity.QuantumTorus.sideSign_neg line 24
4. lemma OAI.ElementaryPositivity.QuantumTorus.simpleOriented_support line 25
5. lemma OAI.ElementaryPositivity.QuantumTorus.simpleOriented_adjoint_fiber line 41
6. def OAI.ElementaryPositivity.QuantumTorus.mutationLinearPiece line 81
7. lemma OAI.ElementaryPositivity.QuantumTorus.mutationLinearPiece_coordinates line 86
8. lemma OAI.ElementaryPositivity.QuantumTorus.mutatedCoordinate_off line 98
9. lemma OAI.ElementaryPositivity.QuantumTorus.mutatedCoordinate_at line 106
10. lemma OAI.ElementaryPositivity.QuantumTorus.mutated_nonpDegree line 139
11. lemma OAI.ElementaryPositivity.QuantumTorus.mutationLinearPiece_span line 148
12. lemma OAI.ElementaryPositivity.QuantumTorus.mutated_span line 160
13. lemma OAI.ElementaryPositivity.QuantumTorus.mutation_root_image line 169