OAI/Combinatorics/Chromatic/Walls/ForwardInventoryRotation.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.TriangularDynamics.levelGaps line 14
2. def OAI.ElementaryPositivity.TriangularDynamics.forwardInventory line 16
3. lemma OAI.ElementaryPositivity.TriangularDynamics.forwardInventory_level_nodup line 19
4. lemma OAI.ElementaryPositivity.TriangularDynamics.levelGaps_root_mem line 23
5. lemma OAI.ElementaryPositivity.TriangularDynamics.forwardInventory_root_mem line 27
6. lemma OAI.ElementaryPositivity.TriangularDynamics.pairwise_distinct line 31
7. lemma OAI.ElementaryPositivity.TriangularDynamics.forwardInventory_rotation line 47
8. def OAI.ElementaryPositivity.QuantumTorus.pivotMap line 114
9. lemma OAI.ElementaryPositivity.QuantumTorus.pivot_involutive line 132
10. lemma OAI.ElementaryPositivity.QuantumTorus.pivot_single line 146
11. lemma OAI.ElementaryPositivity.QuantumTorus.mutatedRoots_realIndependent line 172
12. lemma OAI.ElementaryPositivity.QuantumTorus.rootDegreeCovector_exists line 192