OAI/Combinatorics/Progressions/Estimates/SharedWidthPreparedLateToleranceFreeTrimSource.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.PreparedModularGeneralDirectDetectionFreeTrimPreparedSharedWidthInterface line 80
2. theorem OAI.Erdos3.VectorPolynomial.exists_preparedModularGeneralDirectDetectionLateFloorFreeTrim_sharedWidth line 162
3. def OAI.Erdos3.VectorPolynomial.PreparedModularGeneralCenteredDetectionFreeTrimSharedWidthInterface line 549
4. theorem OAI.Erdos3.VectorPolynomial.preparedModularGeneralCenteredDetectionFreeTrimSharedWidth_of_direct line 640
5. def OAI.Erdos3.VectorPolynomial.SharedWidthDetectedCanonicalLateToleranceFreeTrimPreparedStatement line 739
6. theorem OAI.Erdos3.VectorPolynomial.exists_sharedWidth_detected_canonical_late_tolerance_free_trim_prepared line 881
7. def OAI.Erdos3.VectorPolynomial.SharedWidthPreparedLateToleranceFreeTrimSourceStatement line 1079
8. theorem OAI.Erdos3.VectorPolynomial.exists_sharedWidth_prepared_late_tolerance_free_trim_source line 1219