OAI/NumberTheory/Ostmann/Arithmetic/HistoryPairBulkCoordinatesMatching.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Ostmann.Arithmetic.HistoryPairBulkCoordinates.RootMatching line 12
2. theorem OAI.Ostmann.Arithmetic.HistoryPairBulkCoordinates.RootMatching.key_eq line 18
3. theorem OAI.Ostmann.Arithmetic.HistoryPairBulkCoordinates.right_nonbulk_not_mem line 26
4. def OAI.Ostmann.Arithmetic.HistoryPairBulkCoordinates.insertBulk line 33
5. theorem OAI.Ostmann.Arithmetic.HistoryPairBulkCoordinates.insertBulk_left line 38
6. theorem OAI.Ostmann.Arithmetic.HistoryPairBulkCoordinates.insertBulk_right line 46
7. theorem OAI.Ostmann.Arithmetic.HistoryPairBulkCoordinates.insertBulk_frozen line 53
8. theorem OAI.Ostmann.Arithmetic.HistoryPairBulkCoordinates.sourceBounds line 58