OAI/NumberTheory/Ostmann/Arithmetic/MovingBulkNodup.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Bulk labels remain distinct throughout the actual coherent sampled tree

  1. theorem OAI.Ostmann.MovingSlotData.regularLists_bulk_nodup line 11