OAI/Combinatorics/Chromatic/GradedAlgebra/SeriesApproximation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ElementaryPositivity.QuantumTorus.PrecisionTest line 13
2. def OAI.ElementaryPositivity.QuantumTorus.TestAgreement line 15
3. def OAI.ElementaryPositivity.QuantumTorus.InPrecisionClosure line 19
4. lemma OAI.ElementaryPositivity.QuantumTorus.testAgreement_refl line 23
5. lemma OAI.ElementaryPositivity.QuantumTorus.TestAgreement.trans line 26
6. lemma OAI.ElementaryPositivity.QuantumTorus.inPrecisionClosure_self line 31
7. lemma OAI.ElementaryPositivity.QuantumTorus.InPrecisionClosure.mono line 35
8. lemma OAI.ElementaryPositivity.QuantumTorus.SeriesConverges.testAgreement line 42
9. lemma OAI.ElementaryPositivity.QuantumTorus.InPrecisionClosure.of_converges line 55
10. def OAI.ElementaryPositivity.QuantumTorus.precisionApprox line 66
11. lemma OAI.ElementaryPositivity.QuantumTorus.precisionApprox_mem line 69
12. lemma OAI.ElementaryPositivity.QuantumTorus.precisionApprox_agrees line 72
13. lemma OAI.ElementaryPositivity.QuantumTorus.precisionApprox_converges line 76