OAI/Combinatorics/Chromatic/GradedAlgebra/MutationCoordinates.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.QuantumTorus.simpleRoot line 13
2. def OAI.ElementaryPositivity.QuantumTorus.nonpDegree line 14
3. def OAI.ElementaryPositivity.QuantumTorus.fiberUpper line 18
4. def OAI.ElementaryPositivity.QuantumTorus.fiberCone line 22
5. lemma OAI.ElementaryPositivity.QuantumTorus.root_coordinates line 32
6. lemma OAI.ElementaryPositivity.QuantumTorus.nonpDegree_root_nonneg line 39
7. lemma OAI.ElementaryPositivity.QuantumTorus.nonpDegree_root_eq line 48
8. lemma OAI.ElementaryPositivity.QuantumTorus.nonp_zero_root line 55
9. lemma OAI.ElementaryPositivity.QuantumTorus.nonp_positive_off_cut line 75