OAI/Combinatorics/Chromatic/QuantumTorus/OrdinaryElementaryExpressions.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.QuantumTorus.ElementaryExpr.ordinary line 14
2. lemma OAI.ElementaryPositivity.QuantumTorus.elementary_isHomogeneous line 22
3. lemma OAI.ElementaryPositivity.QuantumTorus.ElementaryExpr.ordinary_homogeneous line 30
4. lemma OAI.ElementaryPositivity.QuantumTorus.ElementaryExpr.ordinary_cast line 40
5. def OAI.ElementaryPositivity.QuantumTorus.ElementaryExpr.natural line 43
6. def OAI.ElementaryPositivity.QuantumTorus.ElementaryExpr.integer line 47
7. lemma OAI.ElementaryPositivity.QuantumTorus.ElementaryExpr.ordinary_natural line 51
8. lemma OAI.ElementaryPositivity.QuantumTorus.ElementaryExpr.ordinary_integer line 57
9. lemma OAI.ElementaryPositivity.QuantumTorus.ElementaryExpr.exists_power line 63
10. lemma OAI.ElementaryPositivity.QuantumTorus.ElementaryExpr.exists_product line 74
11. lemma OAI.ElementaryPositivity.QuantumTorus.homogeneousExpression_representation line 86