OAI/Combinatorics/Progressions/Estimates/AllocatedCanonicalSliceConstructedModelSource.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.allocatedCanonicalSlice_model_source_of_length line 105
2. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedCanonicalSlice_bounded_ambient line 333
3. theorem OAI.Erdos3.VectorPolynomial.allocatedCanonicalSlice_constructed_model_source line 507