OAI/NumberTheory/Ostmann/Arithmetic/HistoryCRTIntegrationModulusBoundBasic.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Ostmann.Arithmetic.HistoryCRTIntegration.factorBound_root line 15
2. lemma OAI.Ostmann.Arithmetic.HistoryCRTIntegration.factorBound_internalSlot line 22
3. lemma OAI.Ostmann.Arithmetic.HistoryCRTIntegration.internal_card_le_divisorCost line 34
4. lemma OAI.Ostmann.Arithmetic.HistoryCRTIntegration.representative_card_le line 42
5. lemma OAI.Ostmann.Arithmetic.HistoryCRTIntegration.representative_prime_le line 48
6. lemma OAI.Ostmann.Arithmetic.HistoryCRTIntegration.rootModulus_le line 57
7. lemma OAI.Ostmann.Arithmetic.HistoryCRTIntegration.outsideModulus_le line 66
8. lemma OAI.Ostmann.Arithmetic.HistoryCRTIntegration.representativeModulus_le line 75