OAI/NumberTheory/Ostmann/Arithmetic/HistoryCRTProjection.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.HistoryCRTProjection.unitPairMap line 10
2. def OAI.Ostmann.Arithmetic.HistoryCRTProjection.mixedPairMap line 13
3. theorem OAI.Ostmann.Arithmetic.HistoryCRTProjection.unitPairMap_surjective line 16
4. theorem OAI.Ostmann.Arithmetic.HistoryCRTProjection.mixedPairMap_surjective line 23
5. theorem OAI.Ostmann.Arithmetic.HistoryCRTProjection.unitPair_fiber_card line 30
6. theorem OAI.Ostmann.Arithmetic.HistoryCRTProjection.unit_pair_average line 34
7. def OAI.Ostmann.Arithmetic.HistoryCRTProjection.mixedPairHom line 38
8. theorem OAI.Ostmann.Arithmetic.HistoryCRTProjection.mixedPair_fiber_card line 42
9. theorem OAI.Ostmann.Arithmetic.HistoryCRTProjection.mixed_pair_average line 46