OAI/Combinatorics/Chromatic/QuantumTorus/TorusContinuity.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.QuantumTorus.TorusConverges line 18
2. lemma OAI.ElementaryPositivity.QuantumTorus.torusConverges_const line 21
3. lemma OAI.ElementaryPositivity.QuantumTorus.TorusConverges.add line 24
4. lemma OAI.ElementaryPositivity.QuantumTorus.TorusConverges.sub line 29
5. lemma OAI.ElementaryPositivity.QuantumTorus.TorusConverges.sum line 36
6. lemma OAI.ElementaryPositivity.QuantumTorus.torus_mul_finite line 44
7. lemma OAI.ElementaryPositivity.QuantumTorus.TorusConverges.mul_of_support line 56
8. lemma OAI.ElementaryPositivity.QuantumTorus.rootGrade_support line 74
9. lemma OAI.ElementaryPositivity.QuantumTorus.TorusConverges.mul_graded line 81
10. lemma OAI.ElementaryPositivity.QuantumTorus.TorusConverges.filter line 91