OAI/NumberTheory/Ostmann/Arithmetic/HistoryGiantOriginalMeanChoicesDefs.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Ostmann.Arithmetic.HistoryGiantOriginalMeanFactorization.PrimeReference line 20
2. def OAI.Ostmann.Arithmetic.HistoryGiantOriginalMeanFactorization.primeReferenceMain line 28
3. structure OAI.Ostmann.Arithmetic.HistoryGiantOriginalMeanFactorization.MixedReference line 35
4. def OAI.Ostmann.Arithmetic.HistoryGiantOriginalMeanFactorization.mixedReferenceMain line 43
5. def OAI.Ostmann.Arithmetic.HistoryGiantOriginalMeanFactorization.choicesPairSum line 50
6. theorem OAI.Ostmann.Arithmetic.HistoryGiantOriginalMeanFactorization.choicesPairSum_error_le line 54