OAI/Combinatorics/Chromatic/Walls/GeometricMutationLines.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.QuantumTorus.realShearCovector_add line 14
2. lemma OAI.ElementaryPositivity.QuantumTorus.realShearCovector_smul line 19
3. lemma OAI.ElementaryPositivity.QuantumTorus.realShearCovector_incoming line 25
4. lemma OAI.ElementaryPositivity.QuantumTorus.realShearCovector_incidence line 38
5. def OAI.ElementaryPositivity.QuantumTorus.realSideCovector line 49
6. lemma OAI.ElementaryPositivity.QuantumTorus.realMutationCovector_eq_side line 51
7. lemma OAI.ElementaryPositivity.QuantumTorus.realSideCovector_incoming_line line 64
8. lemma OAI.ElementaryPositivity.QuantumTorus.realSideCovector_incidence line 73
9. lemma OAI.ElementaryPositivity.QuantumTorus.realMutationCovector_incoming_line line 79
10. lemma OAI.ElementaryPositivity.QuantumTorus.mutationLinearPiece_positive_ray line 97
11. lemma OAI.ElementaryPositivity.QuantumTorus.mutationCompletion_ray_support line 107
12. lemma OAI.ElementaryPositivity.QuantumTorus.actualMutatedWall_ray_support line 134
13. lemma OAI.ElementaryPositivity.QuantumTorus.realSideCovector_mutated_incidence line 148