OAI/Combinatorics/Chromatic/QuantumTorus/PureProductSplit.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.QuantumTorus.ordered_filter_partition line 15
2. lemma OAI.ElementaryPositivity.QuantumTorus.alternating_int_swap line 33
3. lemma OAI.ElementaryPositivity.QuantumTorus.ordered_pure_partition line 38
4. lemma OAI.ElementaryPositivity.QuantumTorus.ray_nonp_zero line 75
5. lemma OAI.ElementaryPositivity.QuantumTorus.ray_nonp_pos line 81
6. lemma OAI.ElementaryPositivity.QuantumTorus.pureFace_of_strict_positive line 89
7. lemma OAI.ElementaryPositivity.QuantumTorus.pureFace_of_strict_zero line 107
8. lemma OAI.ElementaryPositivity.QuantumTorus.pureFace_list_nonpure line 121
9. lemma OAI.ElementaryPositivity.QuantumTorus.pureFace_list_pure line 136