OAI/NumberTheory/Ostmann/Arithmetic/BulkSlotNodup.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Distinct selected bulk labels in the concrete leaf constructor

  1. theorem OAI.Ostmann.mem_flatten_bulkSlotLeaves line 12
  2. theorem OAI.Ostmann.bulkSlotLeaves_nodup line 34
  3. theorem OAI.Ostmann.buildMovingSlotData_root_bulk_nodup line 64
  4. theorem OAI.Ostmann.buildMovingSlotData_bulk_nodup line 85
  5. theorem OAI.Ostmann.bulk_value_injective line 105