OAI/Combinatorics/Chromatic/QuantumTorus/MutationConvexSigns.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.QuantumTorus.realShearVector line 12
2. lemma OAI.ElementaryPositivity.QuantumTorus.realShearCovector_eval line 13
3. lemma OAI.ElementaryPositivity.QuantumTorus.mutated_pos_of_nonneg line 19
4. lemma OAI.ElementaryPositivity.QuantumTorus.mutated_pos_of_nonpos line 32
5. lemma OAI.ElementaryPositivity.QuantumTorus.real_convex_pos line 50
6. lemma OAI.ElementaryPositivity.QuantumTorus.mutation_segment_with_both line 59
7. lemma OAI.ElementaryPositivity.QuantumTorus.mutation_segment_same_side line 77