OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkSupportConversePlanPositive.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.HistoryBulkSupportConversePlan.rootCode line 12
2. def OAI.Ostmann.Arithmetic.HistoryBulkSupportConversePlan.TreeCodeGiantsAgree line 16
3. theorem OAI.Ostmann.Arithmetic.HistoryBulkSupportConversePlan.TreeCodeGiantsAgree.root line 25
4. theorem OAI.Ostmann.Arithmetic.HistoryBulkSupportConversePlan.execute_rebuild_giantsAgree line 33
5. def OAI.Ostmann.Arithmetic.HistoryBulkSupportConversePlan.CodePivotsPositive line 94
6. theorem OAI.Ostmann.Arithmetic.HistoryBulkSupportConversePlan.TreeCodeGiantsAgree.pivotsPositive_iff line 99
7. theorem OAI.Ostmann.Arithmetic.HistoryBulkSupportConversePlan.execute_pivotsPositive_iff_rebuild line 114