OAI/Combinatorics/Progressions/Estimates/PreparedSourceGeometryNormalizedPatchConclusion.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Conclusion.relativePatchSliceConclusion_of_actual_prepared_candidate line 84
2. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.relativePatchSliceConclusion_of_normalized_prepared_degreeRule line 298
3. theorem OAI.Erdos3.VectorPolynomial.relativePatchSliceConclusion_of_normalized_ready line 508
4. theorem OAI.Erdos3.VectorPolynomial.relativePatchSliceConclusion_of_prepared_source_geometry line 721