OAI/NumberTheory/Ostmann/Arithmetic/HistoryPairBulkCoordinatesPermutation.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Ostmann.Arithmetic.HistoryPairBulkCoordinates.matching_of_assignmentsline 14 - theorem
OAI.Ostmann.Arithmetic.HistoryPairBulkCoordinates.leafBulkPermutation_bulk_iffline 33 - def
OAI.Ostmann.Arithmetic.HistoryPairBulkCoordinates.permutationMatchingline 47 - theorem
OAI.Ostmann.Arithmetic.HistoryPairBulkCoordinates.ordered_right_keyline 64 - theorem
OAI.Ostmann.Arithmetic.HistoryPairBulkCoordinates.insertOrdered_rightline 86