OAI/Combinatorics/LowSpaceSubsetSum/Compression/CompressionPassLedger.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Paying for all stopped compression joins with the source ledger

  1. theorem OAI.LowSpaceSubsetSum.CompressionData.sum_pass_allowance line 12
  2. theorem OAI.LowSpaceSubsetSum.CompressionData.sum_pass_allowance_scale line 22