OAI/NumberTheory/Ostmann/Arithmetic/IndexedBulkDistinctness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Bulk collision removal on the original tree-and-word positions

  1. theorem OAI.Ostmann.bulk_distinctness_removal_indexed line 11
  2. theorem OAI.Ostmann.original_bulk_distinctness_removal_indexed line 39