OAI/Combinatorics/Chromatic/GradedAlgebra/HomogeneousElementaryExpressions.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.ElementaryPositivity.QuantumTorus.ElementaryExpr line 13
2. def OAI.ElementaryPositivity.QuantumTorus.ElementaryExpr.eval line 27
3. def OAI.ElementaryPositivity.QuantumTorus.CutSupported line 35
4. lemma OAI.ElementaryPositivity.QuantumTorus.cutSupported_zero line 38
5. lemma OAI.ElementaryPositivity.QuantumTorus.cutSupported_one line 40
6. lemma OAI.ElementaryPositivity.QuantumTorus.cutSupported_add line 46
7. lemma OAI.ElementaryPositivity.QuantumTorus.cutSupported_neg line 52
8. lemma OAI.ElementaryPositivity.QuantumTorus.cutSupported_mul line 56
9. lemma OAI.ElementaryPositivity.QuantumTorus.independentElement_cutSupported line 64
10. lemma OAI.ElementaryPositivity.QuantumTorus.ElementaryExpr.cutSupported line 81
11. lemma OAI.ElementaryPositivity.QuantumTorus.ElementaryExpr.rotation line 92
12. def OAI.ElementaryPositivity.QuantumTorus.NearCut line 121
13. lemma OAI.ElementaryPositivity.QuantumTorus.root_eval_split line 126
14. lemma OAI.ElementaryPositivity.QuantumTorus.nearCut_fiber_negative line 135
15. lemma OAI.ElementaryPositivity.QuantumTorus.nearCut_noncut_wall line 177