OAI/NumberTheory/Jacobsthal/Estimates/ActualPatternClass.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.ErdosVarianceSmallModel.coordinateUnit line 13
2. def OAI.Erdos970.ErdosVarianceSmallModel.liftedNumeratorUnit line 21
3. def OAI.Erdos970.ErdosVarianceSmallModel.restrictionUnit line 27
4. def OAI.Erdos970.ErdosVarianceSmallModel.patternClass line 32
5. theorem OAI.Erdos970.ErdosVarianceSmallModel.patternClass_components line 37
6. theorem OAI.Erdos970.ErdosVarianceSmallModel.patternClass_coprime line 45
7. theorem OAI.Erdos970.ErdosVarianceSmallModel.actual_pattern_class line 67