OAI/NumberTheory/Ostmann/Arithmetic/HistoryPairMixedReplacementCorrectedSample.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.HistoryPairSmoothXi.pairedDiagonalHKeys line 14
2. def OAI.Ostmann.Arithmetic.HistoryPairSmoothXi.pairedDiagonalUKeys line 17
3. theorem OAI.Ostmann.Arithmetic.HistoryPairSmoothXi.pairedDiagonalHKeys_length line 20
4. theorem OAI.Ostmann.Arithmetic.HistoryPairSmoothXi.pairedDiagonalUKeys_length line 24
5. def OAI.Ostmann.Arithmetic.HistoryPairSmoothXi.pairedDiagonalCellCenter line 28
6. def OAI.Ostmann.Arithmetic.HistoryPairSmoothXi.pairedDiagonalCellKey line 32
7. def OAI.Ostmann.Arithmetic.HistoryPairSmoothXi.pairedRootCounterpart line 36
8. theorem OAI.Ostmann.Arithmetic.HistoryPairSmoothXi.pairedRootCounterpart_pullback line 42
9. theorem OAI.Ostmann.Arithmetic.HistoryPairSmoothXi.pairedRootCounterpart_integer_sample line 51
10. theorem OAI.Ostmann.Arithmetic.HistoryPairSmoothXi.correctedPairedRealXi_diagonal_integer_sample line 63