OAI/Combinatorics/Chromatic/GradedAlgebra/TruncatedPrecisionClosure.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ElementaryPositivity.QuantumTorus.RootClosedThrough line 15
2. lemma OAI.ElementaryPositivity.QuantumTorus.RootClosedThrough.congr line 18
3. lemma OAI.ElementaryPositivity.QuantumTorus.InPrecisionClosure.cut line 24
4. lemma OAI.ElementaryPositivity.QuantumTorus.rootClosedThrough_self line 35
5. lemma OAI.ElementaryPositivity.QuantumTorus.RootClosedThrough.mono line 38
6. lemma OAI.ElementaryPositivity.QuantumTorus.rootClosedThrough_approx_exists line 42
7. def OAI.ElementaryPositivity.QuantumTorus.rootApprox line 47
8. lemma OAI.ElementaryPositivity.QuantumTorus.rootApprox_mem line 50
9. lemma OAI.ElementaryPositivity.QuantumTorus.rootApprox_converges line 53
10. lemma OAI.ElementaryPositivity.QuantumTorus.RootClosedThrough.of_converges line 62
11. lemma OAI.ElementaryPositivity.QuantumTorus.RootClosedThrough.zeroFactor line 76