OAI/NumberTheory/Ostmann/Arithmetic/HistorySignedDecodeRebuild.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.HistorySignedDecode.SignedHistory.IntegralGuard line 9
2. def OAI.Ostmann.Arithmetic.HistorySignedDecode.SignedHistory.PivotsPositive line 19
3. theorem OAI.Ostmann.Arithmetic.HistorySignedDecode.SignedHistory.PositiveIntegral.integralGuard line 23
4. def OAI.Ostmann.Arithmetic.HistorySignedDecode.rebuild line 30
5. theorem OAI.Ostmann.Arithmetic.HistorySignedDecode.rebuild_root line 37
6. theorem OAI.Ostmann.Arithmetic.HistorySignedDecode.rebuild_decodeHistory line 41
7. theorem OAI.Ostmann.Arithmetic.HistorySignedDecode.rebuild_nonnegative_of_pivotsPositive line 50
8. theorem OAI.Ostmann.Arithmetic.HistorySignedDecode.rebuild_positiveIntegral line 58