OAI/NumberTheory/Ostmann/Arithmetic/HistoryCRTIntegrationBasic.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.Arithmetic.HistoryCRTIntegration.UnitPair line 12
2. abbrev OAI.Ostmann.Arithmetic.HistoryCRTIntegration.MixedPair line 13
3. instance OAI.Ostmann.Arithmetic.HistoryCRTIntegration.product_neZero line 15
4. def OAI.Ostmann.Arithmetic.HistoryCRTIntegration.unitPairEquiv line 18
5. abbrev OAI.Ostmann.Arithmetic.HistoryCRTIntegration.mixedPairEquiv line 24
6. theorem OAI.Ostmann.Arithmetic.HistoryCRTIntegration.unitPairEquiv_fst_coe line 29
7. theorem OAI.Ostmann.Arithmetic.HistoryCRTIntegration.unitPairEquiv_snd_coe line 37
8. theorem OAI.Ostmann.Arithmetic.HistoryCRTIntegration.average_pi_product line 44
9. theorem OAI.Ostmann.Arithmetic.HistoryCRTIntegration.unit_joint_average line 52
10. theorem OAI.Ostmann.Arithmetic.HistoryCRTIntegration.mixed_joint_average line 58
11. theorem OAI.Ostmann.Arithmetic.HistoryCRTIntegration.unit_product_average line 64
12. theorem OAI.Ostmann.Arithmetic.HistoryCRTIntegration.mixed_product_average line 70
13. theorem OAI.Ostmann.Arithmetic.HistoryCRTIntegration.unitPair_card line 76
14. theorem OAI.Ostmann.Arithmetic.HistoryCRTIntegration.mixedPair_card line 80