OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkSupportConverseSkeleton.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Ostmann.Arithmetic.HistoryBulkSupportConverse.RootStatic line 13
2. structure OAI.Ostmann.Arithmetic.HistoryBulkSupportConverse.NodeStatic line 19
3. def OAI.Ostmann.Arithmetic.HistoryBulkSupportConverse.StaticSkeleton line 28
4. theorem OAI.Ostmann.Arithmetic.HistoryBulkSupportConverse.StaticSkeleton.root line 34
5. theorem OAI.Ostmann.Arithmetic.HistoryBulkSupportConverse.rootStatic_of_supported line 40
6. theorem OAI.Ostmann.Arithmetic.HistoryBulkSupportConverse.staticSkeleton_of_supported line 45
7. theorem OAI.Ostmann.Arithmetic.HistoryBulkSupportConverse.NodeStatic.bulk_products line 57
8. theorem OAI.Ostmann.Arithmetic.HistoryBulkSupportConverse.frequencyLeaves_product_coe_static line 66
9. theorem OAI.Ostmann.Arithmetic.HistoryBulkSupportConverse.frequencyLeaves_child_products_static line 83