OAI/NumberTheory/Ostmann/Arithmetic/HistoryDiagonalCorrectedOriginalMeanEnergyBasic.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.HistoryDiagonalCorrectedOriginalMean.smallCounterpartCoordinate line 17
2. def OAI.Ostmann.Arithmetic.HistoryDiagonalCorrectedOriginalMean.SmallCounterpartCompatible line 22
3. def OAI.Ostmann.Arithmetic.HistoryDiagonalCorrectedOriginalMean.reconstructSmallCounterpart line 26
4. theorem OAI.Ostmann.Arithmetic.HistoryDiagonalCorrectedOriginalMean.smallCounterpartCoordinate_eq line 31
5. theorem OAI.Ostmann.Arithmetic.HistoryDiagonalCorrectedOriginalMean.counterpartCompatible_iff_small line 44
6. theorem OAI.Ostmann.Arithmetic.HistoryDiagonalCorrectedOriginalMean.reconstructCounterpart_eq_small line 61
7. def OAI.Ostmann.Arithmetic.HistoryDiagonalCorrectedOriginalMean.counterpartCurrentAssignment line 77
8. theorem OAI.Ostmann.Arithmetic.HistoryDiagonalCorrectedOriginalMean.counterpartCurrentAssignment_outer line 85
9. theorem OAI.Ostmann.Arithmetic.HistoryDiagonalCorrectedOriginalMean.counterpartCurrentAssignment_small line 92