OAI/Combinatorics/Progressions/Estimates/SharedWidthPreparedModularGeneralDirectDetectionFreeTrim.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.AllocatedPreparedNativeInterfaceGeneralSharedWidth line 73
2. theorem OAI.Erdos3.VectorPolynomial.allocatedPreparedNativeInterfaceGeneral_of_geometry_sharedWidth line 305
3. theorem OAI.Erdos3.VectorPolynomial.allocatedPreparedNativeInterfaceGeneral_of_nonempty_geometry_sharedWidth line 366
4. theorem OAI.Erdos3.VectorPolynomial.preparedModularGeneralDirectDetectionAmbient_sharedWidth line 462
5. theorem OAI.Erdos3.VectorPolynomial.preparedModularGeneralDetector_required_sharedWidth_side line 757
6. theorem OAI.Erdos3.VectorPolynomial.preparedModularGeneralDetectorConstants_required_sharedWidth_side line 786
7. def OAI.Erdos3.VectorPolynomial.PreparedModularGeneralDirectDetectionFreeTrimSharedWidthInterface line 873
8. theorem OAI.Erdos3.VectorPolynomial.preparedModularGeneralDirectDetectionFreeTrimSharedWidthInterface_of_geometry line 983