OAI/NumberTheory/Ostmann/Conclusion/BulkPermutation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.Conclusion.BulkPosition line 12
2. def OAI.Ostmann.Conclusion.bulkPositionPermutation line 14
3. theorem OAI.Ostmann.Conclusion.bulkPositionPermutation_source line 17
4. def OAI.Ostmann.Conclusion.bulkAssignmentPermutation line 27
5. theorem OAI.Ostmann.Conclusion.bulkAssignmentPermutation_mass line 33
6. theorem OAI.Ostmann.Conclusion.initial_bulk_origin_lt line 40
7. theorem OAI.Ostmann.Conclusion.current_bulk_source line 45
8. def OAI.Ostmann.Conclusion.currentBulkAssignmentPermutation line 54