OAI/Combinatorics/Progressions/Dynamics/PreparedModularCanonicalDetectorResourceBudget.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Erdos3.VectorPolynomial.PreparedModularCanonicalDetectorResourceConstants line 10
2. structure OAI.Erdos3.VectorPolynomial.PreparedModularCanonicalDetectorResources line 25
3. def OAI.Erdos3.VectorPolynomial.PreparedModularCanonicalDetectorResources.toList line 55
4. def OAI.Erdos3.VectorPolynomial.PreparedModularCanonicalDetectorResources.total line 58
5. def OAI.Erdos3.VectorPolynomial.PreparedModularCanonicalDetectorResources.map line 61
6. structure OAI.Erdos3.VectorPolynomial.PreparedModularCanonicalDetectorResources.Bounds line 90
7. theorem OAI.Erdos3.VectorPolynomial.PreparedModularCanonicalDetectorResources.bounds_of_list line 118
8. theorem OAI.Erdos3.VectorPolynomial.PreparedModularCanonicalDetectorResources.total_map line 122
9. def OAI.Erdos3.VectorPolynomial.preparedModularCanonicalDetectorResources line 129
10. theorem OAI.Erdos3.VectorPolynomial.preparedModularCanonicalDetectorResources_map line 160
11. theorem OAI.Erdos3.VectorPolynomial.exists_preparedModularCanonicalDetector_resource_budget line 169