OAI/Combinatorics/Chromatic/QuantumTorus/IndependentSetElements.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.QuantumTorus.IsIndependent line 14
2. def OAI.ElementaryPositivity.QuantumTorus.setMonomial line 17
3. def OAI.ElementaryPositivity.QuantumTorus.independentTerm line 20
4. def OAI.ElementaryPositivity.QuantumTorus.independentElement line 23
5. lemma OAI.ElementaryPositivity.QuantumTorus.independent_sum_iff line 26
6. lemma OAI.ElementaryPositivity.QuantumTorus.sum_labels_disjSum line 54
7. lemma OAI.ElementaryPositivity.QuantumTorus.independent_sum_decomposition line 58
8. abbrev OAI.ElementaryPositivity.QuantumTorus.Compatible line 80
9. lemma OAI.ElementaryPositivity.QuantumTorus.compatible_add line 83
10. lemma OAI.ElementaryPositivity.QuantumTorus.finset_fin_three line 92
11. lemma OAI.ElementaryPositivity.QuantumTorus.independent_triple_sum line 95